Commit 2023-11-17 19:26 b1febe50

View on Github →

refactor: rename Submodule.ofLe to Submodule.inclusion (#8470) This matches Set.inclusion, Subring.inclusion, Subalgebra.inclusion, etc. Also renames the homOfLe spellings in Algebra/Lie to match. Note that we leave LieSubalgebra.ofLe, as this is a completely different statement! As requested by @alreadydone.

Estimated changes

Modified Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

Modified Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

Modified Mathlib/Algebra/Category/ModuleCat/Subobject.lean

Modified Mathlib/Algebra/Lie/Semisimple.lean

Modified Mathlib/Algebra/Lie/Solvable.lean

Modified Mathlib/Algebra/Lie/Subalgebra.lean

deleted theorem LieSubalgebra.coe_homOfLe

added theorem LieSubalgebra.coe_inclusion

modified theorem LieSubalgebra.coe_ofLe

modified theorem LieSubalgebra.equivOfLe_apply

deleted def LieSubalgebra.homOfLe

deleted theorem LieSubalgebra.homOfLe_apply

deleted theorem LieSubalgebra.homOfLe_injective

added def LieSubalgebra.inclusion

added theorem LieSubalgebra.inclusion_apply

added theorem LieSubalgebra.inclusion_injective

Modified Mathlib/Algebra/Lie/Submodule.lean

deleted theorem LieIdeal.coe_homOfLe

added theorem LieIdeal.coe_inclusion

deleted def LieIdeal.homOfLe

deleted theorem LieIdeal.homOfLe_apply

deleted theorem LieIdeal.homOfLe_injective

added def LieIdeal.inclusion

added theorem LieIdeal.inclusion_apply

added theorem LieIdeal.inclusion_injective

deleted theorem LieSubmodule.coe_homOfLe

added theorem LieSubmodule.coe_inclusion

deleted def LieSubmodule.homOfLe

deleted theorem LieSubmodule.homOfLe_apply

deleted theorem LieSubmodule.homOfLe_injective

added def LieSubmodule.inclusion

added theorem LieSubmodule.inclusion_apply

added theorem LieSubmodule.inclusion_injective

Modified Mathlib/Algebra/Module/Submodule/LinearMap.lean

added theorem Submodule.coe_inclusion

deleted theorem Submodule.coe_ofLe

added def Submodule.inclusion

added theorem Submodule.inclusion_apply

added theorem Submodule.inclusion_injective

deleted def Submodule.ofLe

deleted theorem Submodule.ofLe_apply

deleted theorem Submodule.ofLe_injective

added theorem Submodule.subtype_comp_inclusion

deleted theorem Submodule.subtype_comp_ofLe

Modified Mathlib/Algebra/Star/NonUnitalSubalgebra.lean

Modified Mathlib/Analysis/Convex/Cone/Extension.lean

Modified Mathlib/LinearAlgebra/Basic.lean

deleted theorem LinearMap.submoduleImage_apply_ofLe

added theorem LinearMap.submoduleImage_apply_of_le

added theorem Submodule.ker_inclusion

deleted theorem Submodule.ker_ofLe

added theorem Submodule.map_subtype_range_inclusion

deleted theorem Submodule.map_subtype_range_ofLe

added theorem Submodule.range_inclusion

deleted theorem Submodule.range_ofLe

Modified Mathlib/LinearAlgebra/Basis.lean

Modified Mathlib/LinearAlgebra/Dimension.lean

Modified Mathlib/LinearAlgebra/FreeModule/PID.lean

Modified Mathlib/LinearAlgebra/Isomorphisms.lean

Modified Mathlib/LinearAlgebra/LinearPMap.lean

added theorem LinearPMap.apply_comp_inclusion

deleted theorem LinearPMap.apply_comp_ofLe

Modified Mathlib/RingTheory/Artinian.lean

Modified Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean