Theorem Matrix.GeneralLinearGroup.fin_two_smul_prod

Modification history

2026-04-19 16:47
Mathlib/Topology/Compactification/OnePoint/ProjectiveLine.lean
refactor(OnePoint/ProjectiveLine): use Pi instead of Prod (#37696) …
Modified Matrix.GeneralLinearGroup.fin_two_smul_prodView on Github →
2025-08-19 14:37
Mathlib/Topology/Compactification/OnePoint/ProjectiveLine.lean
feat(LinearAlgebra/Projectivization): GL(V) action (#26811) …
Added Matrix.GeneralLinearGroup.fin_two_smul_prodView on Github →