Commit 2025-01-26 18:07 e7678994

View on Github →

feat(Algebra): Mul/RingEquivs between center and Module.End (#20721)

Estimated changes

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

deleted def ModuleCat.endMulEquiv

added def ModuleCat.endRingEquiv

Modified Mathlib/Algebra/Module/Equiv/Basic.lean

added def LinearEquiv.arrowCongrAddEquiv

added def LinearEquiv.conjRingEquiv

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

added def Subring.centerCongr

added def Subring.centerToMulOpposite

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

added def Subsemiring.centerCongr

added def Subsemiring.centerToMulOpposite

Modified Mathlib/GroupTheory/Subgroup/Center.lean

added def Subgroup.centerCongr

added def Subgroup.centerToMulOpposite

Modified Mathlib/GroupTheory/Submonoid/Center.lean

added theorem MulEquivClass.apply_mem_center

added theorem MulEquivClass.apply_mem_center_iff

added theorem MulOpposite.op_mem_center_iff

added theorem MulOpposite.unop_mem_center_iff

added def Submonoid.centerCongr

added def Submonoid.centerToMulOpposite

added def Subsemigroup.centerCongr

added def Subsemigroup.centerToMulOpposite

Modified Mathlib/RepresentationTheory/Character.lean

Modified Mathlib/RepresentationTheory/FDRep.lean

deleted theorem FDRep.endMulEquiv_comp_ρ

deleted theorem FDRep.endMulEquiv_symm_comp_ρ

added theorem FDRep.endRingEquiv_comp_ρ

added theorem FDRep.endRingEquiv_symm_comp_ρ

Modified Mathlib/RepresentationTheory/Rep.lean

Modified Mathlib/RingTheory/NonUnitalSubring/Basic.lean

added def NonUnitalSubring.centerCongr

added def NonUnitalSubring.centerToMulOpposite

Modified Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean

added def NonUnitalSubsemiring.centerCongr

added def NonUnitalSubsemiring.centerToMulOpposite