Commit 2026-07-24 09:53 c8f8b4a3

View on Github →

chore(Order): fix defs with underscore in their names (#41878) Per naming convention, defs should not have underscores in their name. This is also counted as strong technical debt, according to the counter we have 493 right now. This PR fixes all of them in Mathlib/Order except one, namely RelIso.Simps.symm_apply, which is a bit weird. All renames here are quite simple, just go from snake_case to lowerCamelCase (+ add deprecations). If this PR looks good, i would be happy to do this to the (vast majority of) other defs with underscore in mathlib. :)

Estimated changes

Modified Mathlib/Algebra/Lie/Semisimple/Basic.lean

Modified Mathlib/Data/Set/Lattice.lean

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean

Modified Mathlib/Order/BooleanGenerators.lean

added def IsCompactlyGenerated.BooleanGenerators.booleanAlgebraOfSSupEqTop

deleted def IsCompactlyGenerated.BooleanGenerators.booleanAlgebra_of_sSup_eq_top

added def IsCompactlyGenerated.BooleanGenerators.distribLatticeOfSSupEqTop

deleted def IsCompactlyGenerated.BooleanGenerators.distribLattice_of_sSup_eq_top

Modified Mathlib/Order/Category/NonemptyFinLinOrd.lean

added def Fin.homSucc

deleted def Fin.hom_succ

Modified Mathlib/Order/Filter/Ker.lean

added def Filter.giPrincipalKer

deleted def Filter.gi_principal_ker

modified theorem Filter.ker_eq_univ

modified theorem Filter.ker_inf

modified theorem Filter.ker_mono

modified theorem Filter.ker_principal

modified theorem Filter.ker_surjective

modified theorem Filter.ker_top

Modified Mathlib/Order/GaloisConnection/Basic.lean

added def gciIciSInf

deleted def gci_Ici_sInf

added def giSSupIic

deleted def gi_sSup_Iic

Modified Mathlib/Order/LiminfLimsup.lean