Theorem ciInf_prod

Modification history

2026-09-01 10:16

Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean

chore(ConditionallyCompleteLattice/Indexed): dualize (#38938)

Deleted ciInf_prod View on Github →

2026-03-04 14:59

Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean

feat(NumberTheory/Height/Basic): add {mul|log}Height_comp_le, {mul|log}Height_fun_mul_eq (#35408) …

Added ciInf_prod View on Github →