Theorem Finite.ciInf_le

Modification history

2026-03-03 11:03
Mathlib/Data/Fintype/Order.lean
feat(Data/Fintype/Order): add API for ciSup with finite indexing type (#35260) …
Modified Finite.ciInf_leView on Github →
2025-08-11 08:45
Mathlib/Order/ConditionallyCompleteLattice/Finset.lean
feat: the Geck Construction yields trace-free matrices (#27831) …
Added Finite.ciInf_leView on Github →