Theorem Subgroup.unop_normalizer

Modification history

2026-03-23 08:24

Mathlib/Algebra/Group/Subgroup/MulOpposite.lean

feat(Algebra/Group/Subgroup/Defs): merge `setNormalizer` into `normalizer` (#36852) …

Modified Subgroup.unop_normalizer View on Github →

2024-08-27 20:26

Mathlib/Algebra/Group/Subgroup/MulOpposite.lean

feat(Subgroup/MulOpposite): add Normal instance (#15497) …

Added Subgroup.unop_normalizer View on Github →