Theorem Multiplicative.isNormalSubgroup

Modification history

2023-01-27 13:20

Mathlib/Deprecated/Subgroup.lean

feat: port `Deprecated.Subgroup` (#1876)

Added Multiplicative.isNormalSubgroup View on Github →