Theorem MulAction.IwasawaStructure.commutator_le

Modification history

2025-02-07 14:21

Mathlib/GroupTheory/GroupAction/Iwasawa.lean

feat(GroupTheory/GroupAction/Iwasawa): the Iwasawa criterion for simplicity (#12048) …

Added MulAction.IwasawaStructure.commutator_le View on Github →