Theorem Submonoid.mem_pos

Modification history

2024-09-01 19:15
Mathlib/Algebra/Order/GroupWithZero/Submonoid.lean
chore(Algebra/Order/Monoid/Submonoid): Don't import `GroupWithZero` (#16381) …
Modified Submonoid.mem_posView 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_posView on Github →
2024-02-13 21:51
Mathlib/GroupTheory/Submonoid/Operations.lean
feat: Submonoid of nonnegative elements (#10209) …
Added Submonoid.mem_posView on Github →