Theorem Pi.mulSingle_le_one

Modification history

2024-10-04 04:46
Mathlib/Algebra/Order/Pi.lean
feat: Order properties of `Pi.single` (#17281) …
Added Pi.mulSingle_le_oneView on Github →