Theorem MulOpposite.unop_mem_center_iff

Modification history

2025-01-26 18:07
Mathlib/GroupTheory/Submonoid/Center.lean
feat(Algebra): `Mul/RingEquiv`s between `center` and `Module.End` (#20721)
Added MulOpposite.unop_mem_center_iffView on Github →