Commit 2026-09-20 11:52 b0df0c4b

View on Github →

style: fix a few instances of 'leading by' (#43995) These should have been caught by lint-style.py, but were not due to a bug in the script. Some of these would be fixed by the auto-formatter; others might not.

Estimated changes

Modified Mathlib/Analysis/Asymptotics/Arith.lean

modified theorem Asymptotics.isBigOWith_abs_left

modified theorem Asymptotics.isBigOWith_abs_right

modified theorem Asymptotics.isBigO_abs_left

modified theorem Asymptotics.isBigO_abs_right

modified theorem Asymptotics.isLittleO_abs_left

modified theorem Asymptotics.isLittleO_abs_right

Modified Mathlib/Data/Quot.lean

Modified Mathlib/GroupTheory/Perm/Support.lean

modified theorem Equiv.Perm.Disjoint.mul_left

Modified Mathlib/LinearAlgebra/Basis/Defs.lean

modified theorem Module.Basis.reindex_apply

Modified Mathlib/LinearAlgebra/Matrix/Determinant/Bird/Defs.lean

Modified Mathlib/Logic/Encodable/Basic.lean

Modified Mathlib/MeasureTheory/Function/LpSeminorm/Monotonicity.lean

Modified Mathlib/ModelTheory/Satisfiability.lean

modified theorem Cardinal.empty_theory_categorical

Modified Mathlib/NumberTheory/PellMatiyasevic.lean

modified theorem Pell.dz_val

Modified Mathlib/RingTheory/FractionalIdeal/Basic.lean

modified theorem FractionalIdeal.coe_natCast

Modified Mathlib/SetTheory/Ordinal/Veblen.lean

modified theorem Ordinal.gamma_add_one_eq_nfp

modified theorem Ordinal.gamma_succ_eq_nfp

Modified Mathlib/Tactic/Linarith/Lemmas.lean

modified theorem Mathlib.Tactic.Linarith.mul_nonpos