Commit 2026-04-19 16:47 2c53994e

View on Github →

refactor(OnePoint/ProjectiveLine): use Pi instead of Prod (#37696) At the moment OnePoint.equivProjectivization identifies the one-point compactification of K with the projective space on K x K. This is slightly inconvenient since most of mathlib's linear algebra prefers Fin n → K. This PR uses the Pi type instead of the product. This is preparatory to adding more material about fixed points of Moebius transformations, etc, in future PR's.

Estimated changes

Modified Mathlib/Topology/Compactification/OnePoint/ProjectiveLine.lean

added theorem Matrix.GeneralLinearGroup.fin_two_smul

modified theorem Matrix.GeneralLinearGroup.fin_two_smul_prod

modified theorem Matrix.fin_two_smul_prod

added theorem Matrix.mulVec_fin_two

modified def OnePoint.equivProjectivization

added theorem OnePoint.equivProjectivization_smul

modified theorem OnePoint.equivProjectivization_symm_apply_mk