Def Submonoid.isPrimal

Modification history

2025-01-31 09:33

Mathlib/Algebra/Group/Submonoid/Membership.lean

chore(Submonoid/Membership): don't import `MonoidWithZero` (#20748) …

Modified Submonoid.isPrimal View on Github →

2024-02-12 20:59

Mathlib/GroupTheory/Submonoid/Membership.lean

feat: introduce `IsRelPrime` and `DecompositionMonoid` and refactor (#10327) …

Added Submonoid.isPrimal View on Github →