Def Submonoid.oneLE

Modification history

2024-02-25 10:47

Mathlib/GroupTheory/Submonoid/Operations.lean

chore: split `Order`ed instances for subobjects into separate files (#10900) …

Modified Submonoid.oneLE View on Github →

2024-02-13 21:51

Mathlib/GroupTheory/Submonoid/Operations.lean

feat: Submonoid of nonnegative elements (#10209) …

Added Submonoid.oneLE View on Github →