Theorem Sylow.smul_eq_iff_mem_normalizer

Modification history

2024-11-08 14:58

Mathlib/GroupTheory/Sylow.lean

refactor(GroupTheory/Sylow): use namespacing and dot-notation (#18750) …

Modified Sylow.smul_eq_iff_mem_normalizer View on Github →

2023-05-29 09:35

Mathlib/GroupTheory/Sylow.lean

feat: port GroupTheory.Sylow (#4387)

Added Sylow.smul_eq_iff_mem_normalizer View on Github →