Theorem inf_one

Modification history

2026-10-13 18:29
Mathlib/Algebra/Order/IsBotOne.lean
feat: add Semilattice lemmas for `IsBotOneClass` (#42538) …
Added inf_oneView on Github →