Theorem one_not_mem_iff

Modification history

2025-05-25 12:30
Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean
chore(*): not_mem/nmem -> notMem (#25159)
Deleted one_not_mem_iffView on Github →
2025-05-13 08:28
Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean
chore: remove `CanonicallyOrdered{Mul, Add}.toOrderBot` (#24094) …
Modified one_not_mem_iffView on Github →
2025-02-11 10:41
Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean
chore: golf theorems using `⊥ = 1` def-eq (#21203) …
Modified one_not_mem_iffView on Github →
2024-08-31 20:17
Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean
feat: add `bot_not_mem_iff` for `OrderBot` (#16336)
Added one_not_mem_iffView on Github →