Theorem OnePoint.smul_infty_def

Modification history

2025-09-03 18:14
Mathlib/Topology/Compactification/OnePoint/ProjectiveLine.lean
feat(Compactification/OnePoint): classify GL2 elements by fixed points (#28552) …
Modified OnePoint.smul_infty_defView on Github →
2025-08-19 14:37
Mathlib/Topology/Compactification/OnePoint/ProjectiveLine.lean
feat(LinearAlgebra/Projectivization): GL(V) action (#26811) …
Added OnePoint.smul_infty_defView on Github →