Theorem Matrix.mulVec_fin_two

Modification history

2026-04-19 16:47
Mathlib/Topology/Compactification/OnePoint/ProjectiveLine.lean
refactor(OnePoint/ProjectiveLine): use Pi instead of Prod (#37696) …
Added Matrix.mulVec_fin_twoView on Github →