Theorem Pi.mulSingle_le_mulSingle

Modification history

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