Theorem OnePoint.equivProjectivization_symm_apply_mk

Modification history

2026-04-19 16:47
Mathlib/Topology/Compactification/OnePoint/ProjectiveLine.lean
refactor(OnePoint/ProjectiveLine): use Pi instead of Prod (#37696) …
Modified OnePoint.equivProjectivization_symm_apply_mkView on Github →
2024-10-24 19:02
Mathlib/Topology/Compactification/OnePointEquiv.lean
feat: Equivalence between OnePoint K and projective line over field K (#17266) …
Added OnePoint.equivProjectivization_symm_apply_mkView on Github →