Commits
Branch selector
User selector
Commit History
Commits on Feb 23, 2024
feat: another characterization of filtered categories in terms of type-valued limits (leanprover-community#10665)
feat(AlgebraicGeometry/EllipticCurve/Projective): implement equations and nonsingularity for projective coordinates (leanprover-community#9416)
feat(FieldTheory/Separable): add result on
Associated
andPolynomial.Separable
(leanprover-community#10897)feat(AlgebraicGeometry/EllipticCurve/Jacobian): implement equations and nonsingularity for Jacobian coordinates (leanprover-community#9432)
feat(GroupTheory/Exponent): lemmas around Monoid.exponent and Subgroup/Submonoid (leanprover-community#10598)
feat: Proof of Hermite theorem on number fields of bounded discriminant (leanprover-community#10030)
feat: between star ordered rings, star-preserving ring homomorphisms preserve order (leanprover-community#10563)
Feb 23, 2024
Commits on Feb 22, 2024
Feb 22, 2024 feat:
arith_mult
: anaesop
tactic for provingIsMultiplicative
statements (leanprover-community#9310)feat: add
IsUnit.mem_unitary_of_star_mul_self
and protect some.star
lemmas (leanprover-community#10855)feat: extend convergence of integrals against peak functions to noncompact settings (leanprover-community#10829)
feat(Algebra/CharP/IntermediateField): characteristic of intermediate fields (leanprover-community#10839)
feat: add lemma
LieAlgebra.IsKilling.eq_zero_of_apply_eq_zero_of_mem_rootSpaceProductNegSelf
(leanprover-community#10803)feat: add versions of the monotone convergence theorem for the Bochner integral (leanprover-community#10793)