mathlib
mathlib copied to clipboard
leanprover-community
Lean 3's obsolete mathematical components library: please use mathlib4
Informally, this is the "minimum distance", though "minimum" makes sense mainly only in the finite context. This is analogous to diam in some sense. We provide finset and set versions...
* The new `cont_diff_within_at_succ_iff_has_fderiv_within_at'` generalizes `cont_diff_within_at.has_fderiv_within_at_nhds` and `cont_diff_within_at_succ_iff_has_fderiv_within_at_of_mem` * Prove that `has_fderiv_within_at` and `cont_diff_within_at` are not dependent on adding a single point to the set * Add some more lemmas...
This splits `data.set.pointwise` and `data.finset.pointwise` each into several smaller files. This allows us to remove or defer some imports, e.g. of `order.well_founded_set` and of `algebra.big_operators.basic`. No changes to statements of...
Proof by induction on the number of summands. finset.sym is used to sum over. It means we have access to the finset tooling to rewrite it, and it's one of...
Add lemmas that, in a real normed space, the sets of points on the same side of an affine subspace as a given point, or on the opposite side from...
This PR defines triangular matrices based on block-triangular matrices. --- - [x] depends on: #14035 - [x] depends on: #16150 [](https://gitpod.io/from-referrer/)
Add a definition of (bundled) subgroupoid and prove some of their basic properties. --- [](https://gitpod.io/from-referrer/)
--- [](https://gitpod.io/from-referrer/)
In this PR we define the conductor ideal and prove some basic results about it. In a later PR (#16870), these will be used to prove the Dedekind-Kummer theorem in...
--- See also comments [on Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/ideals.20in.20non-comm.20rings/near/284039475) [](https://gitpod.io/from-referrer/)
Metadata
Owner
Metadata
Lean 3's obsolete mathematical components library: please use mathlib4