noncomputable def projective_transform {α : Type u_1} [Field α] (p : α × α) (q : α × α) (h : p ≠ q) : (α × α × α) ≃ₗ[α] α × α × α

Equations

• One or more equations did not get rendered due to their size.

theorem project_p {α : Type u_1} [Field α] (p : α × α) (q : α × α) (h : p ≠ q) : (projective_transform p q h) (p.1, p.2, 1) = (1, 0, 0)

theorem project_q {α : Type u_1} [Field α] (p : α × α) (q : α × α) (h : p ≠ q) : (projective_transform p q h) (q.1, q.2, 1) = (0, 1, 0)

theorem of_line {α : Type u_1} [Field α] (p : α × α) (q : α × α) (h : p ≠ q) (x : α × α × α) (h₂ : x ∈ ↑(Submodule.pair p q)) : (projective_transform p q h) x ∈ ↑(Submodule.infinity α)

theorem of_infinity {α : Type u_1} [Field α] (p : α × α) (q : α × α) (h : p ≠ q) (x : α × α × α) (h₂ : x ∈ ↑(Submodule.infinity α)) : (LinearEquiv.symm (projective_transform p q h)) x ∈ ↑(Submodule.pair p q)

theorem non_erasing {α : Type u_1} [Field α] (p : α × α) (q : α × α) (x : α × α) (h : p ≠ q) (h₂ : x ∉ Line.of p q h) : ((projective_transform p q h) (x.1, x.2, 1)).2.2 ≠ 0