Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_atom.inf_eq_bot_of_ne

Modification history

2021-11-23 13:11
src/order/atoms.lean
refactor(*): split `order_{top,bot}` from `lattice` hierarchy (#9891) …
Modified is_atom.inf_eq_bot_of_neView on Github →
2021-01-06 02:30
src/order/atoms.lean
feat(order/atoms): Pairwise coprime (#5596) …
Added is_atom.inf_eq_bot_of_neView on Github →