Theorems · Theorem · general topology

OnePoint.equivProjectivization_symm_apply_mk

∀ (K : Type u_1) [inst : DivisionRing K] [inst_1 : DecidableEq K] (v : Fin 2 → K) (h : v ≠ 0),
  (OnePoint.equivProjectivization K).symm (Projectivization.mk K v h) =
    if v 1 = 0 then OnePoint.infty else ↑((v 1)⁻¹ * v 0)

Defined in

Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Cited by

3 results in Mathlib

Foundations

Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DivisionRingDecidableEq