Theorem WellFoundedLT.induction_bot

Modification history

2025-12-26 18:30
Mathlib/Order/BoundedOrder/Lattice.lean
refactor(Order/BoundedOrder/Lattice): use `to_dual` (#33268) …
Deleted WellFoundedLT.induction_botView on Github →
2025-05-03 07:23
Mathlib/Order/BoundedOrder/Lattice.lean
feat(Algebra): finiteness of associated primes (#24242) …
Added WellFoundedLT.induction_botView on Github →