Theorem Submonoid.mem_oneLE

Modification history

2025-01-03 23:29
Mathlib/Algebra/Order/Monoid/Submonoid.lean
chore(Algebra): Improve attribute generation (#20451) …
Modified Submonoid.mem_oneLEView on Github →
2024-02-25 10:47
Mathlib/GroupTheory/Submonoid/Operations.lean
chore: split `Order`ed instances for subobjects into separate files (#10900) …
Modified Submonoid.mem_oneLEView on Github →
2024-02-15 19:00
Mathlib/GroupTheory/Submonoid/Operations.lean
feat: `ℝ≥0` is a star-ordered ring (#10547) …
Modified Submonoid.mem_oneLEView on Github →
2024-02-13 21:51
Mathlib/GroupTheory/Submonoid/Operations.lean
feat: Submonoid of nonnegative elements (#10209) …
Added Submonoid.mem_oneLEView on Github →