Commit 2025-09-19 16:11 8de03293

View on Github →

chore(Algebra): avoid duplicating proofs by reusing existing theorems or lemmas (#27847)

Estimated changes

Modified Archive/Imo/Imo1972Q5.lean

Modified Archive/Imo/Imo2015Q6.lean

Modified Mathlib/Algebra/Homology/Embedding/Extend.lean

Modified Mathlib/Algebra/MvPolynomial/Rename.lean

Modified Mathlib/Algebra/Order/AbsoluteValue/Basic.lean

Modified Mathlib/Algebra/Order/Archimedean/Class.lean

Modified Mathlib/Algebra/Order/BigOperators/Expect.lean

Modified Mathlib/Algebra/Order/BigOperators/Group/Finset.lean

Modified Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean

Modified Mathlib/Algebra/Order/Group/Abs.lean

modified theorem mabs_mul'

deleted theorem mabs_mul

Modified Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean

modified theorem Rat.lt_one_iff_num_lt_denom

Modified Mathlib/Algebra/Polynomial/Degree/Lemmas.lean

deleted theorem Polynomial.coeff_mul_of_natDegree_le

Modified Mathlib/Algebra/Polynomial/Monic.lean

deleted theorem Polynomial.ne_zero_of_ne_zero_of_monic

Modified Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean

Modified Mathlib/Analysis/MeanInequalities.lean

Modified Mathlib/Analysis/Normed/Lp/lpSpace.lean

Modified Mathlib/Data/NNRat/Defs.lean

Modified Mathlib/MeasureTheory/Function/Jacobian.lean

Modified Mathlib/NumberTheory/Pell.lean

Modified Mathlib/RingTheory/Polynomial/Basic.lean

Modified Mathlib/Tactic/ComputeDegree.lean

Modified Mathlib/Topology/Algebra/Order/Group.lean

Modified Mathlib/Topology/MetricSpace/Algebra.lean

Modified MathlibTest/GCongr/inequalities.lean

Modified MathlibTest/GRewrite.lean