Commit 2025-08-01 23:04 211b784a

View on Github →

feat(*): add simp/gcongr attrs and use them (#27718) Also weaken assumptions of Polynomial.X_pow_sub_one_mul_prod_cyclotomic_eq_X_pow_sub_one_of_dvd.

Estimated changes

Modified Mathlib/Algebra/Divisibility/Basic.lean

modified theorem pow_dvd_pow_of_dvd

added theorem pow_dvd_pow_of_dvd_of_le

Modified Mathlib/Algebra/GCDMonoid/Nat.lean

Modified Mathlib/Algebra/Order/Group/Unbundled/Int.lean

modified theorem Int.natCast_natAbs

Modified Mathlib/Algebra/Order/Ring/Int.lean

Modified Mathlib/Combinatorics/SimpleGraph/Finite.lean

Modified Mathlib/Data/Finset/Card.lean

Modified Mathlib/Data/Int/Log.lean

Modified Mathlib/Data/Int/ModEq.lean

Modified Mathlib/Data/Multiset/Defs.lean

Modified Mathlib/Data/Nat/Log.lean

added theorem Nat.clog_mono

added theorem Nat.log_mono

Modified Mathlib/Data/Nat/Sqrt.lean

Modified Mathlib/Data/Nat/Squarefree.lean

Modified Mathlib/Data/Nat/Totient.lean

Modified Mathlib/Data/ZMod/Basic.lean

added theorem ZMod.intCast_abs_mod_two

Modified Mathlib/NumberTheory/Divisors.lean

Modified Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean

Modified Mathlib/NumberTheory/PellMatiyasevic.lean

Modified Mathlib/NumberTheory/Zsqrtd/Basic.lean

added theorem Zsqrtd.abs_norm

Modified Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean

Modified Mathlib/RingTheory/Coprime/Lemmas.lean

Modified Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean