Commit 2025-08-20 20:25 f2a71bb8

View on Github →

chore(Algebra): rename snake_case to lowerCamelCase related to Submonoid/Subgroup (#28707) I'm not finding all violations, but these should be apparently not following the naming convention.

Estimated changes

Modified Mathlib/Algebra/Group/Submonoid/Operations.lean

Modified Mathlib/LinearAlgebra/Basis/Submodule.lean

Modified Mathlib/LinearAlgebra/RootSystem/Base.lean

Modified Mathlib/LinearAlgebra/Span/Defs.lean

added theorem Submodule.span_int_eq_addSubgroupClosure

deleted theorem Submodule.span_int_eq_addSubgroup_closure

added theorem Submodule.span_nat_eq_addSubmonoidClosure

deleted theorem Submodule.span_nat_eq_addSubmonoid_closure

Modified Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean

Modified Mathlib/NumberTheory/NumberField/Units/Regulator.lean

Modified Mathlib/RingTheory/Finiteness/Defs.lean

added theorem Submodule.fg_iff_addSubgroup_fg

deleted theorem Submodule.fg_iff_add_subgroup_fg