Commit 2024-12-25 13:01 0137f529

View on Github →

chore(*): use gcongr and omega here and there (#20228)

Estimated changes

Modified Archive/Wiedijk100Theorems/AbelRuffini.lean

Modified Mathlib/Algebra/GeomSum.lean

Modified Mathlib/Algebra/LinearRecurrence.lean

Modified Mathlib/Algebra/MonoidAlgebra/Degree.lean

Modified Mathlib/Algebra/Order/Floor.lean

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

modified theorem abs_add