Theorem Subgroup.Normal.mem_comm_iff

Modification history

2024-07-26 01:01

Mathlib/Algebra/Group/Subgroup/Basic.lean

chore: robustifying for debug.byAsSorry (part 4) (#15125)

Modified Subgroup.Normal.mem_comm_iff View on Github →

2023-01-26 10:26

Mathlib/GroupTheory/Subgroup/Basic.lean

feat: port GroupTheory.Subgroup.Basic (#1797)

Added Subgroup.Normal.mem_comm_iff View on Github →