Theorem Prod.snd_bot

Modification history

2025-12-05 13:19
Mathlib/Order/BoundedOrder/Basic.lean
chore(Order/BoundedOrder/Basic): use `to_dual` (#32377) …
Deleted Prod.snd_botView on Github →
2025-01-21 15:48
Mathlib/Order/BoundedOrder/Basic.lean
feat(IncidenceAlgebra): Euler characteristic of a partial order (#20299) …
Modified Prod.snd_botView on Github →
2023-07-18 03:33
Mathlib/Order/BoundedOrder.lean
feat: CompletelyDistribLattice (#5238) …
Added Prod.snd_botView on Github →