Theorem OnePoint.equivProjectivization_apply_coe

Modification history

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_apply_coeView on Github →