Commit 2025-02-19 09:43 4824fbd1

View on Github →

chore: rename coeSubtype theorems (#22064) A more comprehensive version of #17219.

Estimated changes

Modified Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

deleted theorem NonUnitalSubalgebraClass.coeSubtype

added theorem NonUnitalSubalgebraClass.coe_subtype

Modified Mathlib/Algebra/Algebra/Subalgebra/Unitization.lean

Modified Mathlib/Algebra/Group/Subgroup/Defs.lean

deleted theorem Subgroup.coeSubtype

added theorem Subgroup.coe_subtype

deleted theorem SubgroupClass.coeSubtype

added theorem SubgroupClass.coe_subtype

Modified Mathlib/Algebra/Group/Subgroup/Ker.lean

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

Modified Mathlib/Algebra/Ring/Subring/Defs.lean

deleted theorem Subring.coeSubtype

added theorem Subring.coe_subtype

deleted theorem SubringClass.coeSubtype

added theorem SubringClass.coe_subtype

Modified Mathlib/Algebra/Star/NonUnitalSubalgebra.lean

deleted theorem NonUnitalStarSubalgebraClass.coeSubtype

added theorem NonUnitalStarSubalgebraClass.coe_subtype

Modified Mathlib/GroupTheory/Finiteness.lean

Modified Mathlib/GroupTheory/Goursat.lean

Modified Mathlib/GroupTheory/GroupAction/SubMulAction.lean

Modified Mathlib/GroupTheory/NoncommPiCoprod.lean

Modified Mathlib/GroupTheory/Perm/Centralizer.lean

Modified Mathlib/GroupTheory/Perm/Cycle/Factors.lean

Modified Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

Modified Mathlib/GroupTheory/Sylow.lean

Modified Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean

deleted theorem AffineSubspace.coeSubtype

added theorem AffineSubspace.coe_subtype

Modified Mathlib/ModelTheory/ElementarySubstructures.lean

deleted theorem FirstOrder.Language.ElementarySubstructure.coeSubtype

added theorem FirstOrder.Language.ElementarySubstructure.coe_subtype

Modified Mathlib/ModelTheory/Fraisse.lean

Modified Mathlib/ModelTheory/PartialEquiv.lean

Modified Mathlib/ModelTheory/Substructures.lean

deleted theorem FirstOrder.Language.Substructure.coeSubtype

added theorem FirstOrder.Language.Substructure.coe_subtype

Modified Mathlib/NumberTheory/MulChar/Duality.lean

Modified Mathlib/RingTheory/NonUnitalSubsemiring/Defs.lean

deleted theorem NonUnitalSubsemiringClass.coeSubtype

added theorem NonUnitalSubsemiringClass.coe_subtype

Modified Mathlib/RingTheory/Polynomial/Basic.lean

Modified Mathlib/RingTheory/Valuation/ValuationSubring.lean

Modified Mathlib/Topology/Algebra/Group/Basic.lean