Theorem Subgroup.IsComplement'.card_mul

Modification history

2024-07-18 16:07

Mathlib/GroupTheory/Complement.lean

refactor(GroupTheory/Complement,SchurZassenhaus): Replace `Fintype.card` with `Nat.card` (#14856) …

Modified Subgroup.IsComplement'.card_mul View on Github →

2023-05-29 08:45

Mathlib/GroupTheory/Complement.lean

feat: port GroupTheory.Complement (#4349)

Added Subgroup.IsComplement'.card_mul View on Github →