mathlib
mathlib copied to clipboard
leanprover-community
Lean 3's obsolete mathematical components library: please use mathlib4
--- [](https://gitpod.io/from-referrer/)
I had a go at Minkowski's convex body theorem and it works thanks to @urkud 's pidgeonhole for measurable spaces. My interest is in the applications to number theory, hence...
This introduces three categories of C⋆-algebras (over `ℂ`), namely: * `CStarAlg`: not necessarily unital C⋆-algebras with `non_unital_star_alg_hom`s * `CStarAlg₁`: unital C⋆-algebras with `star_alg_hom`s * `CommCStarAlg₁`: commutative unital C⋆-algebras with `star_alg_hom`s...
- [x] depends on: #16172 - [x] depends on: #16189 --- [](https://gitpod.io/from-referrer/)
Since injective groups are divisible and vice versa, we show `AddCommGroup` has enough "divisibles": for any group $A$, we embed $A$ into $\prod_{f : A \to \mathbb{Q}/\mathbb{Z}} \mathbb{Q}/\mathbb{Z}$, since $\mathbb{Q}/\mathbb{Z}$...
--- The alternative version of `val_min_abs`. Returns integer on the interval `[-n/2, n/2)` instead of the interval `(-n/2, n/2]`. This is what machine integers do, a signed integer is an...
--- [](https://gitpod.io/from-referrer/)
--- - [x] depends on: #13908 - [x] depends on: #13905 - [x] depends on: #13882 - [ ] depends on: #13933 - [x] depends on: #13934 - [x] depends...
This PR adds new ways to construct projective subspaces. This PR also adds lemmas which show that for a projective subspace, any nonzero linear combination of vectors, where each vector...
We add `add is_cyclotomic_extension.equiv`: being a cyclotomic extension is preserved by `alg_equiv`. From flt-regular --- [](https://gitpod.io/from-referrer/)
Metadata
Owner
Metadata
Lean 3's obsolete mathematical components library: please use mathlib4