Theorem Sylow.subtype_injective

Modification history

2024-11-08 14:58

Mathlib/GroupTheory/Sylow.lean

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

Modified Sylow.subtype_injective View on Github →

2023-05-29 09:35

Mathlib/GroupTheory/Sylow.lean

feat: port GroupTheory.Sylow (#4387)

Added Sylow.subtype_injective View on Github →