Theorem Pi.mulSingle_inf

Modification history

2023-05-01 15:10
Mathlib/Algebra/Group/Pi.lean
feat: `f.update i '' Icc a b = Icc (f.update i a) (f.update i b)` (#3747) …
Added Pi.mulSingle_infView on Github →