Commit 2024-11-13 14:41 6d5c720a

View on Github →

chore(Submonoid): make coe projection be a prefix (#18870) Change initialize_simps_projection to use coe as prefix on Submonoid and Subgroup

Estimated changes

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

deleted theorem AlgHom.coe_range

deleted theorem Subalgebra.center_toSubsemiring

deleted theorem Subalgebra.coe_center

deleted theorem Subalgebra.coe_comap

deleted theorem Subalgebra.coe_copy

deleted theorem Subalgebra.coe_map

deleted theorem Subalgebra.map_toSubsemiring

deleted theorem Submodule.coe_toSubalgebra

Modified Mathlib/Algebra/Algebra/Subalgebra/MulOpposite.lean

deleted theorem Subalgebra.op_coe

deleted theorem Subalgebra.unop_coe

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

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

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

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

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

deleted theorem Subring.coe_copy

deleted theorem Subring.coe_mk'

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

deleted theorem Subring.op_coe

deleted theorem Subring.unop_coe

Modified Mathlib/Algebra/Ring/Subsemiring/Basic.lean

deleted theorem RingHom.coe_rangeS

deleted theorem Subsemiring.center_toSubmonoid

deleted theorem Subsemiring.coe_center

deleted theorem Subsemiring.coe_comap

deleted theorem Subsemiring.coe_map

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

deleted theorem Subsemiring.coe_copy

deleted theorem Subsemiring.coe_mk'

Modified Mathlib/Algebra/Ring/Subsemiring/MulOpposite.lean

deleted theorem Subsemiring.op_coe

deleted theorem Subsemiring.unop_coe