Commit 2025-09-02 19:30 fe22cf81

View on Github →

chore: fix names of coe_ lattice lemmas (#29183) This renames Submodule.sInf_coe to Submodule.coe_sInf, which is already the naming pattern used for AddSubmonoid.

Estimated changes

added theorem LieHom.coe_range
deleted theorem LieHom.range_coe
added theorem LieSubalgebra.coe_inf
added theorem LieSubalgebra.coe_sInf
deleted theorem LieSubalgebra.inf_coe
deleted theorem LieSubalgebra.sInf_coe
added theorem LieSubmodule.coe_iInf
added theorem LieSubmodule.coe_inf
added theorem LieSubmodule.coe_sInf
deleted theorem LieSubmodule.iInf_coe
deleted theorem LieSubmodule.inf_coe
deleted theorem LieSubmodule.sInf_coe
added theorem Submodule.coe_iInf
added theorem Submodule.coe_inf
added theorem Submodule.coe_sInf
deleted theorem Submodule.finset_inf_coe
deleted theorem Submodule.iInf_coe
deleted theorem Submodule.inf_coe
deleted theorem Submodule.mem_finset_inf
deleted theorem Submodule.sInf_coe
added theorem LinearMap.coe_range
deleted theorem LinearMap.range_coe
added theorem AffineSubspace.coe_inf
deleted theorem AffineSubspace.inf_coe