Standard Vector Space

This file defines the standard inner product real vector space of dimension two, but we will build this on the complex numbers.

Important definitions

Notation

Implementation Notes

Further Works

theorem Units.coe_div {α : Type u} [DivisionMonoid α] (u₁ : αˣ) (u₂ : αˣ) : ↑(u₁ / u₂) = ↑u₁ / ↑u₂

Alias of Units.val_div_eq_div_val.

theorem SameRay.norm_smul_map_eq {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {M : Type u_2} [AddCommGroup M] [Module ℝ M] {x : E} {y : E} {F : Type u_3} [SMulHomClass F ℝ E M] (f : F) (h : SameRay ℝ x y) : ‖x‖ • f y = ‖y‖ • f x

theorem SameRay.inv_norm_smul_map_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {M : Type u_2} [AddCommGroup M] [Module ℝ M] {x : E} {y : E} {F : Type u_3} [SMulHomClass F ℝ E M] (f : F) (hx : x ≠ 0) (hy : y ≠ 0) (h : SameRay ℝ x y) : ‖x‖⁻¹ • f x = ‖y‖⁻¹ • f y

theorem Module.Ray.map_trans {R : Type u_1} [StrictOrderedCommSemiring R] {M₁ : Type u_2} [AddCommMonoid M₁] [Module R M₁] {M₂ : Type u_3} [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_4} [AddCommMonoid M₃] [Module R M₃] (e₁₂ : M₁ ≃ₗ[R] M₂) (e₂₃ : M₂ ≃ₗ[R] M₃) : Module.Ray.map (e₁₂ ≪≫ₗ e₂₃) = (Module.Ray.map e₁₂).trans (Module.Ray.map e₂₃)

def Projectivization.mapEquiv {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {L : Type u_3} {W : Type u_4} [DivisionRing L] [AddCommGroup W] [Module L W] {σ : K →+* L} {σ' : L →+* K} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (f : V ≃ₛₗ[σ] W) : Projectivization K V ≃ Projectivization L W

An semilinear equivalence of vector spaces induces a equivalence on projective spaces.

Equations

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

@[simp]

theorem Projectivization.mapEquiv_refl {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] : Projectivization.mapEquiv (LinearEquiv.refl K V) = Equiv.refl (Projectivization K V)

@[simp]

theorem Projectivization.mapEquiv_symm {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {L : Type u_3} {W : Type u_4} [DivisionRing L] [AddCommGroup W] [Module L W] {σ : K →+* L} {σ' : L →+* K} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (f : V ≃ₛₗ[σ] W) : (Projectivization.mapEquiv f).symm = Projectivization.mapEquiv (LinearEquiv.symm f)

@[simp]

theorem Projectivization.mapEquiv_trans {K₁ : Type u_5} {V₁ : Type u_6} [Field K₁] [AddCommGroup V₁] [Module K₁ V₁] {K₂ : Type u_7} {V₂ : Type u_8} [Field K₂] [AddCommGroup V₂] [Module K₂ V₂] {K₃ : Type u_9} {V₃ : Type u_10} [Field K₃] [AddCommGroup V₃] [Module K₃ V₃] {σ₁₂ : K₁ →+* K₂} {σ₂₃ : K₂ →+* K₃} {σ₁₃ : K₁ →+* K₃} {σ₂₁ : K₂ →+* K₁} {σ₃₂ : K₃ →+* K₂} {σ₃₁ : K₃ →+* K₁} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} [RingHomInvPair σ₁₃ σ₃₁] {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {re₃₂ : RingHomInvPair σ₃₂ σ₂₃} [RingHomInvPair σ₃₁ σ₁₃] (e₁₂ : V₁ ≃ₛₗ[σ₁₂] V₂) (e₂₃ : V₂ ≃ₛₗ[σ₂₃] V₃) : Projectivization.mapEquiv (LinearEquiv.trans e₁₂ e₂₃) = (Projectivization.mapEquiv e₁₂).trans (Projectivization.mapEquiv e₂₃)

theorem InnerProductSpace.Core.inner_self_eq_norm_mul_norm' {𝕜 : Type u_1} {F : Type u_2} [IsROrC 𝕜] [AddCommGroup F] [Module 𝕜 F] [InnerProductSpace.Core 𝕜 F] (x : F) : inner x x = ↑‖x‖ * ↑‖x‖

theorem InnerProductSpace.Core.inner_self_eq_norm_sq' {𝕜 : Type u_1} {F : Type u_2} [IsROrC 𝕜] [AddCommGroup F] [Module 𝕜 F] [InnerProductSpace.Core 𝕜 F] (x : F) : inner x x = ↑‖x‖ ^ 2

theorem inner_self_eq_norm_mul_norm' {𝕜 : Type u_1} {E : Type u_2} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) : inner x x = ↑‖x‖ * ↑‖x‖

theorem inner_self_eq_norm_sq' {𝕜 : Type u_1} {E : Type u_2} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) : inner x x = ↑‖x‖ ^ 2

def IsROrC.toComplex {𝕜 : Type u_1} [IsROrC 𝕜] (z : 𝕜) : ℂ

Equations

• ↑z = { re := IsROrC.re z, im := IsROrC.im z }

instance IsROrC.instCoeComplex {𝕜 : Type u_1} [IsROrC 𝕜] : Coe 𝕜 ℂ

Equations

• IsROrC.instCoeComplex = { coe := IsROrC.toComplex }

@[simp]

theorem IsROrC.toComplex_eq_self (z : ℂ) : ↑z = z

@[simp]

theorem IsROrC.toComplex_re {𝕜 : Type u_1} [IsROrC 𝕜] (z : 𝕜) : (↑z).re = IsROrC.re z

@[simp]

theorem IsROrC.toComplex_im {𝕜 : Type u_1} [IsROrC 𝕜] (z : 𝕜) : (↑z).im = IsROrC.im z

@[simp]

theorem IsROrC.toComplex_one {𝕜 : Type u_1} [IsROrC 𝕜] : ↑1 = 1

@[simp]

theorem IsROrC.toComplex_zero {𝕜 : Type u_1} [IsROrC 𝕜] : ↑0 = 0

@[simp]

theorem IsROrC.toComplex_mul {𝕜 : Type u_1} [IsROrC 𝕜] (z : 𝕜) (w : 𝕜) : ↑(z * w) = ↑z * ↑w

@[simp]

theorem IsROrC.toComplex_add {𝕜 : Type u_1} [IsROrC 𝕜] (z : 𝕜) (w : 𝕜) : ↑(z + w) = ↑z + ↑w

@[simp]

theorem IsROrC.normSq_toComplex {𝕜 : Type u_1} [IsROrC 𝕜] (z : 𝕜) : Complex.normSq ↑z = IsROrC.normSq z

@[simp]

theorem IsROrC.toComplex_inv {𝕜 : Type u_1} [IsROrC 𝕜] (z : 𝕜) : ↑z⁻¹ = (↑z)⁻¹

@[simp]

theorem IsROrC.abs_toComplex {𝕜 : Type u_1} [IsROrC 𝕜] (z : 𝕜) : Complex.abs ↑z = ‖z‖

instance IsROrC.instSMulComplex {𝕜 : Type u_1} [IsROrC 𝕜] : SMul 𝕜 ℂ

Equations

• IsROrC.instSMulComplex = { smul := fun (x : 𝕜) (z : ℂ) => ↑x * z }

theorem IsROrC.smul_def {𝕜 : Type u_1} [IsROrC 𝕜] (x : 𝕜) (z : ℂ) : x • z = ↑x * z

instance IsROrC.IsROrC.normedSpaceComplex {𝕜 : Type u_1} [IsROrC 𝕜] : NormedSpace 𝕜 ℂ

Equations

• IsROrC.IsROrC.normedSpaceComplex = NormedSpace.mk (_ : ∀ (a : 𝕜) (a_1 : ℂ), ‖↑a * a_1‖ ≤ ‖a‖ * Complex.abs a_1)

structure EuclidGeom.Vec : Type

• fst : ℝ
• snd : ℝ

def EuclidGeom.Vec.equivWithLp : EuclidGeom.Vec ≃ WithLp 2 (ℝ × ℝ)

Equations

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

instance EuclidGeom.Vec.nontrivial : Nontrivial EuclidGeom.Vec

Equations

• EuclidGeom.Vec.nontrivial = (_ : Nontrivial EuclidGeom.Vec)

instance EuclidGeom.Vec.addCommGrop : AddCommGroup EuclidGeom.Vec

Equations

• EuclidGeom.Vec.addCommGrop = Equiv.addCommGroup EuclidGeom.Vec.equivWithLp

instance EuclidGeom.Vec.normedAddCommGroup : NormedAddCommGroup EuclidGeom.Vec

Equations

• EuclidGeom.Vec.normedAddCommGroup = NormedAddCommGroup.mk

theorem EuclidGeom.Vec.norm_def (v : EuclidGeom.Vec) : ‖v‖ = Real.sqrt (v.fst * v.fst + v.snd * v.snd)

theorem EuclidGeom.Vec.norm_sq (v : EuclidGeom.Vec) : ‖v‖ ^ 2 = v.fst * v.fst + v.snd * v.snd

theorem EuclidGeom.Vec.ext {v₁ : EuclidGeom.Vec} {v₂ : EuclidGeom.Vec} (h₁ : v₁.fst = v₂.fst) (h₂ : v₁.snd = v₂.snd) : v₁ = v₂

theorem EuclidGeom.Vec.mk_fst {x : ℝ} {y : ℝ} : { fst := x, snd := y }.fst = x

theorem EuclidGeom.Vec.mk_snd {x : ℝ} {y : ℝ} : { fst := x, snd := y }.snd = y

@[simp]

theorem EuclidGeom.Vec.mk_zero_zero : { fst := 0, snd := 0 } = 0

@[simp]

theorem EuclidGeom.Vec.zero_fst : 0.fst = 0

@[simp]

theorem EuclidGeom.Vec.zero_snd : 0.snd = 0

@[simp]

theorem EuclidGeom.Vec.mk_add_mk (x₁ : ℝ) (x₂ : ℝ) (y₁ : ℝ) (y₂ : ℝ) : { fst := x₁, snd := y₁ } + { fst := x₂, snd := y₂ } = { fst := x₁ + x₂, snd := y₁ + y₂ }

@[simp]

theorem EuclidGeom.Vec.add_fst (v₁ : EuclidGeom.Vec) (v₂ : EuclidGeom.Vec) : (v₁ + v₂).fst = v₁.fst + v₂.fst

@[simp]

theorem EuclidGeom.Vec.add_snd (v₁ : EuclidGeom.Vec) (v₂ : EuclidGeom.Vec) : (v₁ + v₂).snd = v₁.snd + v₂.snd

@[simp]

theorem EuclidGeom.Vec.neg_mk (x : ℝ) (y : ℝ) : -{ fst := x, snd := y } = { fst := -x, snd := -y }

@[simp]

theorem EuclidGeom.Vec.neg_fst (v : EuclidGeom.Vec) : (-v).fst = -v.fst

@[simp]

theorem EuclidGeom.Vec.neg_snd (v : EuclidGeom.Vec) : (-v).snd = -v.snd

instance EuclidGeom.Vec.normedSpace {𝕜 : Type u_1} [IsROrC 𝕜] : NormedSpace 𝕜 EuclidGeom.Vec

Equations

• EuclidGeom.Vec.normedSpace = NormedSpace.mk (_ : ∀ (z : 𝕜) (v : EuclidGeom.Vec), ‖z • v‖ ≤ ‖z‖ * ‖v‖)

theorem EuclidGeom.Vec.complex_smul_def (s : ℂ) (v : EuclidGeom.Vec) : s • v = { fst := s.re * v.fst - s.im * v.snd, snd := s.re * v.snd + s.im * v.fst }

@[simp]

theorem EuclidGeom.Vec.complex_smul_mk (s : ℂ) (x : ℝ) (y : ℝ) : s • { fst := x, snd := y } = { fst := s.re * x - s.im * y, snd := s.re * y + s.im * x }

@[simp]

theorem EuclidGeom.Vec.complex_smul_fst (s : ℂ) (v : EuclidGeom.Vec) : (s • v).fst = s.re * v.fst - s.im * v.snd

@[simp]

theorem EuclidGeom.Vec.complex_smul_snd (s : ℂ) (v : EuclidGeom.Vec) : (s • v).snd = s.re * v.snd + s.im * v.fst

theorem EuclidGeom.Vec.smul_def' (s : ℝ) (v : EuclidGeom.Vec) : s • v = { fst := s * v.fst - 0 * v.snd, snd := s * v.snd + 0 * v.fst }

@[simp]

theorem EuclidGeom.Vec.smul_mk' (s : ℝ) (x : ℝ) (y : ℝ) : s • { fst := x, snd := y } = { fst := s * x - 0 * y, snd := s * y + 0 * x }

@[simp]

theorem EuclidGeom.Vec.smul_fst' (s : ℝ) (v : EuclidGeom.Vec) : (s • v).fst = s * v.fst - 0 * v.snd

@[simp]

theorem EuclidGeom.Vec.smul_snd' (s : ℝ) (v : EuclidGeom.Vec) : (s • v).snd = s * v.snd + 0 * v.fst

theorem EuclidGeom.Vec.smul_def (s : ℝ) (v : EuclidGeom.Vec) : s • v = { fst := s * v.fst, snd := s * v.snd }

@[simp]

theorem EuclidGeom.Vec.smul_mk (s : ℝ) (x : ℝ) (y : ℝ) : s • { fst := x, snd := y } = { fst := s * x, snd := s * y }

@[simp]

theorem EuclidGeom.Vec.smul_fst (s : ℝ) (v : EuclidGeom.Vec) : (s • v).fst = s * v.fst

@[simp]

theorem EuclidGeom.Vec.smul_snd (s : ℝ) (v : EuclidGeom.Vec) : (s • v).snd = s * v.snd

def EuclidGeom.Vec.det : EuclidGeom.Vec →ₗ[ℝ] EuclidGeom.Vec →ₗ[ℝ] ℝ

Equations

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

theorem EuclidGeom.Vec.det_apply (v₁ : EuclidGeom.Vec) (v₂ : EuclidGeom.Vec) : (EuclidGeom.Vec.det v₁) v₂ = v₁.fst * v₂.snd - v₁.snd * v₂.fst

@[simp]

theorem EuclidGeom.Vec.det_self (v : EuclidGeom.Vec) : (EuclidGeom.Vec.det v) v = 0

theorem EuclidGeom.Vec.det_skew (v₁ : EuclidGeom.Vec) (v₂ : EuclidGeom.Vec) : -(EuclidGeom.Vec.det v₁) v₂ = (EuclidGeom.Vec.det v₂) v₁

instance EuclidGeom.Vec.innerProductSpace' : InnerProductSpace ℝ EuclidGeom.Vec

Equations

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

theorem EuclidGeom.Vec.real_inner_apply (v₁ : EuclidGeom.Vec) (v₂ : EuclidGeom.Vec) : inner v₁ v₂ = v₁.fst * v₂.fst + v₁.snd * v₂.snd

instance EuclidGeom.Vec.innerProductSpace : InnerProductSpace ℂ EuclidGeom.Vec

Equations

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

@[simp]

theorem EuclidGeom.Vec.inner_re (v₁ : EuclidGeom.Vec) (v₂ : EuclidGeom.Vec) : (inner v₁ v₂).re = inner v₁ v₂

@[simp]

theorem EuclidGeom.Vec.inner_im (v₁ : EuclidGeom.Vec) (v₂ : EuclidGeom.Vec) : (inner v₁ v₂).im = (EuclidGeom.Vec.det v₁) v₂

theorem EuclidGeom.Vec.complex_inner_apply' (v₁ : EuclidGeom.Vec) (v₂ : EuclidGeom.Vec) : inner v₁ v₂ = { re := inner v₁ v₂, im := (EuclidGeom.Vec.det v₁) v₂ }

theorem EuclidGeom.Vec.complex_inner_apply (v₁ : EuclidGeom.Vec) (v₂ : EuclidGeom.Vec) : inner v₁ v₂ = ↑(inner v₁ v₂) + ↑((EuclidGeom.Vec.det v₁) v₂) * Complex.I

theorem EuclidGeom.Vec.smul_inner (v₁ : EuclidGeom.Vec) (v₂ : EuclidGeom.Vec) : inner v₁ v₂ • v₁ = ‖v₁‖ ^ 2 • v₂

def EuclidGeom.Vec.scaleRotate : ℂ →+* EuclidGeom.Vec →ₗ[ℂ] EuclidGeom.Vec

Equations

• EuclidGeom.Vec.scaleRotate = Module.toModuleEnd ℂ EuclidGeom.Vec

@[simp]

theorem EuclidGeom.Vec.scaleRotate_apply (z : ℂ) (v : EuclidGeom.Vec) : (EuclidGeom.Vec.scaleRotate z) v = z • v

def EuclidGeom.Vec.scaleRotateEquiv : ℂˣ →* EuclidGeom.Vec ≃ₗ[ℂ] EuclidGeom.Vec

Equations

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

@[simp]

theorem EuclidGeom.Vec.scaleRotateEquiv_mk0 (z : ℂ) (hz : z ≠ 0) : ⇑(EuclidGeom.Vec.scaleRotateEquiv (Units.mk0 z hz)) = ⇑(EuclidGeom.Vec.scaleRotate z)

theorem EuclidGeom.Vec.smul_bijective {z : ℂ} (hz : z ≠ 0) : Function.Bijective fun (x : EuclidGeom.Vec) => z • x

def EuclidGeom.Vec.rotate (θ : EuclidGeom.AngValue) : EuclidGeom.Vec ≃ₗ[ℂ] EuclidGeom.Vec

Equations

• EuclidGeom.Vec.rotate θ = EuclidGeom.Vec.scaleRotateEquiv (circle.toUnits (EuclidGeom.AngValue.expMapCircle θ))

@[simp]

theorem EuclidGeom.Vec.rotate_mk (θ : EuclidGeom.AngValue) (x : ℝ) (y : ℝ) : (EuclidGeom.Vec.rotate θ) { fst := x, snd := y } = { fst := EuclidGeom.AngValue.cos θ * x - EuclidGeom.AngValue.sin θ * y, snd := EuclidGeom.AngValue.cos θ * y + EuclidGeom.AngValue.sin θ * x }

@[simp]

theorem EuclidGeom.Vec.rotate_fst (θ : EuclidGeom.AngValue) (v : EuclidGeom.Vec) : ((EuclidGeom.Vec.rotate θ) v).fst = EuclidGeom.AngValue.cos θ * v.fst - EuclidGeom.AngValue.sin θ * v.snd

@[simp]

theorem EuclidGeom.Vec.rotate_snd (θ : EuclidGeom.AngValue) (v : EuclidGeom.Vec) : ((EuclidGeom.Vec.rotate θ) v).snd = EuclidGeom.AngValue.cos θ * v.snd + EuclidGeom.AngValue.sin θ * v.fst

theorem EuclidGeom.Vec.smul_eq_rotate (z : ℂ) (v : EuclidGeom.Vec) : z • v = ‖z‖ • (EuclidGeom.Vec.rotate ∠[Complex.arg z]) v

@[simp]

theorem EuclidGeom.Vec.expMapCircle_smul_eq_rotate (θ : EuclidGeom.AngValue) (v : EuclidGeom.Vec) : EuclidGeom.AngValue.expMapCircle θ • v = (EuclidGeom.Vec.rotate θ) v

@[simp]

theorem LinearEquiv.one_apply {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) : 1 x = x

@[simp]

theorem LinearEquiv.mul_apply {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (f : M ≃ₗ[R] M) (g : M ≃ₗ[R] M) (x : M) : (f * g) x = f (g x)

@[simp]

theorem EuclidGeom.Vec.rotate_zero : EuclidGeom.Vec.rotate 0 = 1

theorem EuclidGeom.Vec.rotate_zero_apply (v : EuclidGeom.Vec) : (EuclidGeom.Vec.rotate 0) v = v

@[simp]

theorem EuclidGeom.Vec.rotate_pi : EuclidGeom.Vec.rotate ∠[Real.pi] = LinearEquiv.neg ℂ

theorem EuclidGeom.Vec.rotate_pi_apply (v : EuclidGeom.Vec) : (EuclidGeom.Vec.rotate ∠[Real.pi]) v = -v

@[simp]

theorem EuclidGeom.Vec.rotate_add (θ : EuclidGeom.AngValue) (ψ : EuclidGeom.AngValue) : EuclidGeom.Vec.rotate (θ + ψ) = EuclidGeom.Vec.rotate θ * EuclidGeom.Vec.rotate ψ

theorem EuclidGeom.Vec.rotate_add_apply (θ : EuclidGeom.AngValue) (ψ : EuclidGeom.AngValue) (v : EuclidGeom.Vec) : (EuclidGeom.Vec.rotate (θ + ψ)) v = (EuclidGeom.Vec.rotate θ) ((EuclidGeom.Vec.rotate ψ) v)

@[simp]

theorem EuclidGeom.Vec.norm_rotate (θ : EuclidGeom.AngValue) (v : EuclidGeom.Vec) : ‖(EuclidGeom.Vec.rotate θ) v‖ = ‖v‖

theorem EuclidGeom.Vec.rotate_eq_zero {θ : EuclidGeom.AngValue} {v : EuclidGeom.Vec} : (EuclidGeom.Vec.rotate θ) v = 0 ↔ v = 0

theorem EuclidGeom.Vec.rotate_ne_zero {θ : EuclidGeom.AngValue} {v : EuclidGeom.Vec} : (EuclidGeom.Vec.rotate θ) v ≠ 0 ↔ v ≠ 0

instance EuclidGeom.Vec.instHDivVecComplex : HDiv EuclidGeom.Vec EuclidGeom.Vec ℂ

Equations

• EuclidGeom.Vec.instHDivVecComplex = { hDiv := fun (v₁ v₂ : EuclidGeom.Vec) => inner v₂ v₁ / ↑‖v₂‖ ^ 2 }

theorem EuclidGeom.Vec.cdiv_def (v₁ : EuclidGeom.Vec) (v₂ : EuclidGeom.Vec) : v₁ / v₂ = inner v₂ v₁ / ↑‖v₂‖ ^ 2

theorem EuclidGeom.Vec.add_cdiv (v₁ : EuclidGeom.Vec) (v₁' : EuclidGeom.Vec) (v₂ : EuclidGeom.Vec) : (v₁ + v₁') / v₂ = v₁ / v₂ + v₁' / v₂

theorem EuclidGeom.Vec.neg_cdiv (v₁ : EuclidGeom.Vec) (v₂ : EuclidGeom.Vec) : -v₁ / v₂ = -(v₁ / v₂)

theorem EuclidGeom.Vec.cdiv_neg (v₁ : EuclidGeom.Vec) (v₂ : EuclidGeom.Vec) : v₁ / -v₂ = -(v₁ / v₂)

theorem EuclidGeom.Vec.sub_cdiv (v₁ : EuclidGeom.Vec) (v₁' : EuclidGeom.Vec) (v₂ : EuclidGeom.Vec) : (v₁ - v₁') / v₂ = v₁ / v₂ - v₁' / v₂

theorem EuclidGeom.Vec.complex_smul_cdiv (z : ℂ) (v₁ : EuclidGeom.Vec) (v₂ : EuclidGeom.Vec) : z • v₁ / v₂ = z * (v₁ / v₂)

theorem EuclidGeom.Vec.mul_cdiv (z : ℂ) (v₁ : EuclidGeom.Vec) (v₂ : EuclidGeom.Vec) : z * (v₁ / v₂) = z • v₁ / v₂

theorem EuclidGeom.Vec.smul_cdiv {𝕜 : Type u_1} [IsROrC 𝕜] (z : 𝕜) (v₁ : EuclidGeom.Vec) (v₂ : EuclidGeom.Vec) : z • v₁ / v₂ = z • (v₁ / v₂)

@[simp]

theorem EuclidGeom.Vec.cdiv_smul_cancel (v₁ : EuclidGeom.Vec) {v₂ : EuclidGeom.Vec} (hv₂ : v₂ ≠ 0) : (v₁ / v₂) • v₂ = v₁

@[simp]

theorem EuclidGeom.Vec.complex_smul_cdiv_cancel (z : ℂ) {v : EuclidGeom.Vec} (hv : v ≠ 0) : z • v / v = z

theorem EuclidGeom.Vec.inner_left_bijective {v : EuclidGeom.Vec} (h : v ≠ 0) : Function.Bijective fun (x : EuclidGeom.Vec) => inner v x

theorem EuclidGeom.Vec.inner_right_bijective {v : EuclidGeom.Vec} (h : v ≠ 0) : Function.Bijective fun (x : EuclidGeom.Vec) => inner x v

@[simp]

theorem EuclidGeom.Vec.complex_inner_eq_zero_iff {v₁ : EuclidGeom.Vec} {v₂ : EuclidGeom.Vec} : inner v₁ v₂ = 0 ↔ v₁ = 0 ∨ v₂ = 0

theorem EuclidGeom.Vec.complex_inner_ne_zero_iff {v₁ : EuclidGeom.Vec} {v₂ : EuclidGeom.Vec} : inner v₁ v₂ ≠ 0 ↔ v₁ ≠ 0 ∧ v₂ ≠ 0

@[simp]

theorem EuclidGeom.Vec.cdiv_eq_zero {v₁ : EuclidGeom.Vec} {v₂ : EuclidGeom.Vec} : v₁ / v₂ = 0 ↔ v₁ = 0 ∨ v₂ = 0

@[simp]

theorem EuclidGeom.Vec.cdiv_zero (v : EuclidGeom.Vec) : v / 0 = 0

@[simp]

theorem EuclidGeom.Vec.zero_cdiv (v : EuclidGeom.Vec) : 0 / v = 0

theorem EuclidGeom.Vec.cdiv_ne_zero {v₁ : EuclidGeom.Vec} {v₂ : EuclidGeom.Vec} : v₁ / v₂ ≠ 0 ↔ v₁ ≠ 0 ∧ v₂ ≠ 0

theorem EuclidGeom.Vec.cdiv_left_inj {v₁ : EuclidGeom.Vec} {v₂ : EuclidGeom.Vec} {v₃ : EuclidGeom.Vec} (hv₃ : v₃ ≠ 0) : v₁ / v₃ = v₂ / v₃ ↔ v₁ = v₂

theorem EuclidGeom.Vec.cdiv_eq_iff {v₁ : EuclidGeom.Vec} {v₂ : EuclidGeom.Vec} {z : ℂ} (hv₂ : v₂ ≠ 0) : v₁ / v₂ = z ↔ v₁ = z • v₂

theorem EuclidGeom.Vec.eq_cdiv_iff {v₁ : EuclidGeom.Vec} {v₂ : EuclidGeom.Vec} {z : ℂ} (hv₂ : v₂ ≠ 0) : z = v₁ / v₂ ↔ z • v₂ = v₁

theorem EuclidGeom.Vec.cdiv_eq_one_iff_eq {v₁ : EuclidGeom.Vec} {v₂ : EuclidGeom.Vec} (hv₂ : v₂ ≠ 0) : v₁ / v₂ = 1 ↔ v₁ = v₂

@[simp]

theorem EuclidGeom.Vec.cdiv_self {v : EuclidGeom.Vec} (hv : v ≠ 0) : v / v = 1

@[simp]

theorem EuclidGeom.Vec.smul_cdiv_cancel {𝕜 : Type u_1} [IsROrC 𝕜] (z : 𝕜) {v : EuclidGeom.Vec} (hv : v ≠ 0) : z • v / v = ↑z

@[simp]

theorem EuclidGeom.Vec.real_smul_cdiv_cancel (z : ℝ) {v : EuclidGeom.Vec} (hv : v ≠ 0) : z • v / v = ↑z

theorem EuclidGeom.Vec.inv_cdiv (v₁ : EuclidGeom.Vec) (v₂ : EuclidGeom.Vec) : (v₁ / v₂)⁻¹ = v₂ / v₁

theorem EuclidGeom.Vec.cdiv_complex_smul (z : ℂ) (v₁ : EuclidGeom.Vec) (v₂ : EuclidGeom.Vec) : v₁ / z • v₂ = z⁻¹ * (v₁ / v₂)

@[simp]

theorem EuclidGeom.Vec.cdiv_smul {𝕜 : Type u_1} [IsROrC 𝕜] (z : 𝕜) (v₁ : EuclidGeom.Vec) (v₂ : EuclidGeom.Vec) : v₁ / z • v₂ = z⁻¹ • (v₁ / v₂)

theorem EuclidGeom.Vec.inner_smul_comm_right (v₁ : EuclidGeom.Vec) (v₂ : EuclidGeom.Vec) (v₃ : EuclidGeom.Vec) : inner v₁ v₂ • v₃ = inner v₁ v₃ • v₂

theorem EuclidGeom.Vec.cdiv_smul_comm (v₁ : EuclidGeom.Vec) (v₂ : EuclidGeom.Vec) (v₃ : EuclidGeom.Vec) : (v₁ / v₂) • v₃ = (v₃ / v₂) • v₁

theorem EuclidGeom.Vec.cdiv_eq_cdiv_iff_cdiv_eq_cdiv {v₁ : EuclidGeom.Vec} {v₂ : EuclidGeom.Vec} {v₃ : EuclidGeom.Vec} {v₄ : EuclidGeom.Vec} (hv₂ : v₂ ≠ 0) (hv₃ : v₃ ≠ 0) : v₁ / v₂ = v₃ / v₄ ↔ v₁ / v₃ = v₂ / v₄

@[simp]

theorem EuclidGeom.Vec.abs_inner (v₁ : EuclidGeom.Vec) (v₂ : EuclidGeom.Vec) : Complex.abs (inner v₁ v₂) = ‖v₁‖ * ‖v₂‖

@[simp]

theorem EuclidGeom.Vec.abs_cdiv (v₁ : EuclidGeom.Vec) (v₂ : EuclidGeom.Vec) : Complex.abs (v₁ / v₂) = ‖v₁‖ / ‖v₂‖

theorem IsROrC.ofReal_eq_complex_coe : IsROrC.ofReal = Complex.ofReal'

theorem EuclidGeom.Vec.real_inner_of_sameRay {v₁ : EuclidGeom.Vec} {v₂ : EuclidGeom.Vec} (h : SameRay ℝ v₁ v₂) : inner v₁ v₂ = ‖v₁‖ * ‖v₂‖

theorem EuclidGeom.Vec.det_of_sameRay {v₁ : EuclidGeom.Vec} {v₂ : EuclidGeom.Vec} (h : SameRay ℝ v₁ v₂) : (EuclidGeom.Vec.det v₁) v₂ = 0

theorem EuclidGeom.Vec.complex_inner_of_sameRay {v₁ : EuclidGeom.Vec} {v₂ : EuclidGeom.Vec} (h : SameRay ℝ v₁ v₂) : inner v₁ v₂ = ↑‖v₁‖ * ↑‖v₂‖

theorem EuclidGeom.Vec.cdiv_of_sameRay {v₁ : EuclidGeom.Vec} {v₂ : EuclidGeom.Vec} (h : SameRay ℝ v₁ v₂) : v₁ / v₂ = ↑(‖v₁‖ / ‖v₂‖)

@[simp]

theorem EuclidGeom.Vec.arg_cdiv (θ : EuclidGeom.AngValue) {v : EuclidGeom.Vec} (hv : v ≠ 0) : ∠[Complex.arg ((EuclidGeom.Vec.rotate θ) v / v)] = θ

@[inline, reducible]

abbrev EuclidGeom.VecND : Type

the class of non-degenerate vectors

Equations

• EuclidGeom.VecND = RayVector ℝ EuclidGeom.Vec

@[inline, reducible]

abbrev EuclidGeom.VecND.mk (v : EuclidGeom.Vec) (hv : v ≠ 0) : EuclidGeom.VecND

Equations

• EuclidGeom.VecND.mk v hv = { val := v, property := hv }

instance EuclidGeom.VecND.instCoeOutVecNDVec : CoeOut EuclidGeom.VecND EuclidGeom.Vec

Equations

• EuclidGeom.VecND.instCoeOutVecNDVec = subtypeCoe

instance EuclidGeom.VecND.instNegVecND : Neg EuclidGeom.VecND

Equations

• EuclidGeom.VecND.instNegVecND = { neg := fun (v : EuclidGeom.VecND) => { val := -↑v, property := (_ : -↑v ≠ 0) } }

@[simp]

theorem EuclidGeom.VecND.ne_zero (x : EuclidGeom.VecND) : ↑x ≠ 0

@[simp]

theorem EuclidGeom.VecND.coe_neg (v : EuclidGeom.VecND) : ↑(-v) = -↑v

instance EuclidGeom.VecND.instNormVecND : Norm EuclidGeom.VecND

Equations

• EuclidGeom.VecND.instNormVecND = { norm := fun (v : EuclidGeom.VecND) => ‖↑v‖ }

@[simp]

theorem EuclidGeom.VecND.norm_coe (v : EuclidGeom.VecND) : ‖↑v‖ = ‖v‖

@[simp]

theorem EuclidGeom.VecND.norm_pos (v : EuclidGeom.VecND) : 0 < ‖v‖

def EuclidGeom.VecND.evalVecNDNorm : Mathlib.Meta.Positivity.PositivityExt

Extension for the positivity tactic.

Equations

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

@[simp]

theorem EuclidGeom.VecND.norm_ne_zero (v : EuclidGeom.VecND) : ‖v‖ ≠ 0

@[simp]

theorem EuclidGeom.VecND.norm_neg (v : EuclidGeom.VecND) : ‖-v‖ = ‖v‖

theorem EuclidGeom.VecND.ext {v₁ : EuclidGeom.VecND} {v₂ : EuclidGeom.VecND} : ↑v₁ = ↑v₂ → v₁ = v₂

theorem EuclidGeom.VecND.coe_inj {v₁ : EuclidGeom.VecND} {v₂ : EuclidGeom.VecND} : ↑v₁ = ↑v₂ ↔ v₁ = v₂

@[simp]

theorem EuclidGeom.VecND.coe_smul {G : Type u_1} [Group G] [DistribMulAction G EuclidGeom.Vec] (g : G) (v : EuclidGeom.VecND) : ↑(g • v) = g • ↑v

@[simp]

theorem EuclidGeom.VecND.coe_vadd {G : Type u_1} [Group G] [DistribMulAction G EuclidGeom.Vec] (g : Additive G) (v : EuclidGeom.VecND) : ↑(g +ᵥ v) = Additive.toMul g • ↑v

theorem EuclidGeom.VecND.smul_def {G : Type u_1} [Group G] [DistribMulAction G EuclidGeom.Vec] (g : G) (v : EuclidGeom.VecND) : g • v = { val := g • ↑v, property := (_ : g • ↑v ≠ 0) }

theorem EuclidGeom.VecND.vadd_def {G : Type u_1} [Group G] [DistribMulAction G EuclidGeom.Vec] (g : Additive G) (v : EuclidGeom.VecND) : g +ᵥ v = { val := Additive.toMul g • ↑v, property := (_ : Additive.toMul g • ↑v ≠ 0) }

theorem EuclidGeom.VecND.mk_neg (v : EuclidGeom.Vec) (hv : v ≠ 0) : { val := -v, property := (_ : -v ≠ 0) } = -{ val := v, property := hv }

@[simp]

theorem EuclidGeom.VecND.mk_neg' (v : EuclidGeom.Vec) (hv : -v ≠ 0) : { val := -v, property := hv } = -{ val := v, property := (_ : v ≠ 0) }

theorem EuclidGeom.VecND.mk_smul {G : Type u_1} [Group G] [DistribMulAction G EuclidGeom.Vec] (g : G) (v : EuclidGeom.Vec) (hv : v ≠ 0) : { val := g • v, property := (_ : g • v ≠ 0) } = g • { val := v, property := hv }

@[simp]

theorem EuclidGeom.VecND.mk_smul' {G : Type u_1} [Group G] [DistribMulAction G EuclidGeom.Vec] (g : G) (v : EuclidGeom.Vec) (hv : g • v ≠ 0) : { val := g • v, property := hv } = g • { val := v, property := (_ : v ≠ 0) }

theorem EuclidGeom.VecND.mk_vadd {G : Type u_1} [Group G] [DistribMulAction G EuclidGeom.Vec] (g : Additive G) (v : EuclidGeom.Vec) (hv : v ≠ 0) : { val := g +ᵥ v, property := (_ : Additive.toMul g • v ≠ 0) } = g +ᵥ { val := v, property := hv }

@[simp]

theorem EuclidGeom.VecND.mk_vadd' {G : Type u_1} [Group G] [DistribMulAction G EuclidGeom.Vec] (g : Additive G) (v : EuclidGeom.Vec) (hv : g +ᵥ v ≠ 0) : { val := g +ᵥ v, property := hv } = g +ᵥ { val := v, property := (_ : v ≠ 0) }

@[simp]

theorem EuclidGeom.VecND.mk_smul₀ {G : Type u_1} [DivisionSemiring G] [Module G EuclidGeom.Vec] [NoZeroSMulDivisors G EuclidGeom.Vec] (g : G) (v : EuclidGeom.Vec) (hv : g • v ≠ 0) : { val := g • v, property := hv } = Units.mk0 g (_ : g ≠ 0) • EuclidGeom.VecND.mk v (_ : v ≠ 0)

@[simp]

theorem EuclidGeom.VecND.neg_smul {R : Type u_1} [Ring R] [Module R EuclidGeom.Vec] (g : Rˣ) (v : EuclidGeom.VecND) : -g • v = -(g • v)

@[simp]

theorem EuclidGeom.VecND.smul_neg {R : Type u_1} [Ring R] [Module R EuclidGeom.Vec] (g : Rˣ) (v : EuclidGeom.VecND) : g • -v = -(g • v)

@[simp]

theorem EuclidGeom.VecND.norm_smul (r : ℝˣ) (v : EuclidGeom.VecND) : ‖r • v‖ = ‖↑r‖ * ‖v‖

instance EuclidGeom.VecND.instNontrivialVecND : Nontrivial EuclidGeom.VecND

Equations

• EuclidGeom.VecND.instNontrivialVecND = (_ : Nontrivial EuclidGeom.VecND)

instance EuclidGeom.VecND.instHDivVecNDUnitsComplexToMonoidToMonoidWithZeroInstSemiringComplex : HDiv EuclidGeom.VecND EuclidGeom.VecND ℂˣ

Equations

• EuclidGeom.VecND.instHDivVecNDUnitsComplexToMonoidToMonoidWithZeroInstSemiringComplex = { hDiv := fun (v₁ v₂ : EuclidGeom.VecND) => Units.mk0 (↑v₁ / ↑v₂) (_ : ↑v₁ / ↑v₂ ≠ 0) }

@[simp]

theorem EuclidGeom.VecND.coe_cdiv (v₁ : EuclidGeom.VecND) (v₂ : EuclidGeom.VecND) : ↑(v₁ / v₂) = ↑v₁ / ↑v₂

theorem EuclidGeom.VecND.smul_cdiv (z : ℂˣ) (v₁ : EuclidGeom.VecND) (v₂ : EuclidGeom.VecND) : z • v₁ / v₂ = z * (v₁ / v₂)

@[simp]

theorem EuclidGeom.VecND.cdiv_smul_cancel (v₁ : EuclidGeom.VecND) (v₂ : EuclidGeom.VecND) : (v₁ / v₂) • v₂ = v₁

@[simp]

theorem EuclidGeom.VecND.smul_cdiv_cancel (z : ℂˣ) (v : EuclidGeom.VecND) : z • v / v = z

instance EuclidGeom.VecND.instAddTorsorAdditiveUnitsComplexToMonoidToMonoidWithZeroInstSemiringComplexVecNDAddGroupInstGroup : AddTorsor (Additive ℂˣ) EuclidGeom.VecND

Equations

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

theorem EuclidGeom.VecND.vsub_def (v₁ : EuclidGeom.VecND) (v₂ : EuclidGeom.VecND) : v₁ -ᵥ v₂ = Additive.ofMul (v₁ / v₂)

theorem EuclidGeom.VecND.rotate_ne_zero (θ : EuclidGeom.AngValue) (v : EuclidGeom.VecND) : (EuclidGeom.Vec.rotate θ) ↑v ≠ 0

def EuclidGeom.VecND.map (e : EuclidGeom.Vec ≃ₗ[ℝ] EuclidGeom.Vec) : EuclidGeom.VecND ≃ EuclidGeom.VecND

Equations

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

def EuclidGeom.VecND.rotate (θ : EuclidGeom.AngValue) : EuclidGeom.VecND ≃ EuclidGeom.VecND

Equations

• EuclidGeom.VecND.rotate θ = EuclidGeom.VecND.map (LinearEquiv.restrictScalars ℝ (EuclidGeom.Vec.rotate θ))

def EuclidGeom.VecND.angle (v₁ : EuclidGeom.VecND) (v₂ : EuclidGeom.VecND) : EuclidGeom.AngValue

Equations

• EuclidGeom.VecND.angle v₁ v₂ = ∠[Complex.arg ↑(Additive.toMul (v₂ -ᵥ v₁))]

def EuclidGeom.VecND.SameDir (v₁ : EuclidGeom.VecND) (v₂ : EuclidGeom.VecND) : Prop

Equations

• EuclidGeom.VecND.SameDir v₁ v₂ = ∃ (x : ℝ), 0 < x ∧ ↑v₁ = x • ↑v₂

@[simp]

theorem EuclidGeom.VecND.sameRay_iff_sameDir {v₁ : EuclidGeom.VecND} {v₂ : EuclidGeom.VecND} : SameRay ℝ ↑v₁ ↑v₂ ↔ EuclidGeom.VecND.SameDir v₁ v₂

theorem EuclidGeom.VecND.SameDir.ofSameRay {v₁ : EuclidGeom.VecND} {v₂ : EuclidGeom.VecND} : SameRay ℝ ↑v₁ ↑v₂ → EuclidGeom.VecND.SameDir v₁ v₂

Alias of the forward direction of EuclidGeom.VecND.sameRay_iff_sameDir.

theorem EuclidGeom.VecND.SameDir.toSameRay {v₁ : EuclidGeom.VecND} {v₂ : EuclidGeom.VecND} : EuclidGeom.VecND.SameDir v₁ v₂ → SameRay ℝ ↑v₁ ↑v₂

Alias of the reverse direction of EuclidGeom.VecND.sameRay_iff_sameDir.

@[simp]

theorem EuclidGeom.VecND.SameDir.refl (v : EuclidGeom.VecND) : EuclidGeom.VecND.SameDir v v

theorem EuclidGeom.VecND.SameDir.rfl {v : EuclidGeom.VecND} : EuclidGeom.VecND.SameDir v v

theorem EuclidGeom.VecND.SameDir.symm {v₁ : EuclidGeom.VecND} {v₂ : EuclidGeom.VecND} (h : EuclidGeom.VecND.SameDir v₁ v₂) : EuclidGeom.VecND.SameDir v₂ v₁

theorem EuclidGeom.VecND.SameDir.trans {v₁ : EuclidGeom.VecND} {v₂ : EuclidGeom.VecND} {v₃ : EuclidGeom.VecND} (h₁ : EuclidGeom.VecND.SameDir v₁ v₂) (h₂ : EuclidGeom.VecND.SameDir v₂ v₃) : EuclidGeom.VecND.SameDir v₁ v₃

@[simp]

theorem EuclidGeom.VecND.sameDir_neg_iff {v₁ : EuclidGeom.VecND} {v₂ : EuclidGeom.VecND} : EuclidGeom.VecND.SameDir (-v₁) (-v₂) ↔ EuclidGeom.VecND.SameDir v₁ v₂

theorem EuclidGeom.VecND.SameDir.neg {v₁ : EuclidGeom.VecND} {v₂ : EuclidGeom.VecND} : EuclidGeom.VecND.SameDir v₁ v₂ → EuclidGeom.VecND.SameDir (-v₁) (-v₂)

Alias of the reverse direction of EuclidGeom.VecND.sameDir_neg_iff.

theorem EuclidGeom.VecND.SameDir.of_neg {v₁ : EuclidGeom.VecND} {v₂ : EuclidGeom.VecND} : EuclidGeom.VecND.SameDir (-v₁) (-v₂) → EuclidGeom.VecND.SameDir v₁ v₂

Alias of the forward direction of EuclidGeom.VecND.sameDir_neg_iff.

theorem EuclidGeom.VecND.sameDir_neg_swap {v₁ : EuclidGeom.VecND} {v₂ : EuclidGeom.VecND} : EuclidGeom.VecND.SameDir (-v₁) v₂ ↔ EuclidGeom.VecND.SameDir v₁ (-v₂)

@[simp]

theorem EuclidGeom.VecND.sameDir_smul_left_iff {v : EuclidGeom.VecND} {r : ℝˣ} : EuclidGeom.VecND.SameDir (r • v) v ↔ 0 < ↑r

@[simp]

theorem EuclidGeom.VecND.sameDir_smul_right_iff {v : EuclidGeom.VecND} {r : ℝˣ} : EuclidGeom.VecND.SameDir v (r • v) ↔ 0 < ↑r

@[simp]

theorem EuclidGeom.VecND.sameRay_neg_smul_left_iff {v : EuclidGeom.VecND} {r : ℝˣ} : EuclidGeom.VecND.SameDir (r • v) (-v) ↔ ↑r < 0

@[simp]

theorem EuclidGeom.VecND.sameRay_neg_smul_right_iff {v : EuclidGeom.VecND} {r : ℝˣ} : EuclidGeom.VecND.SameDir (-v) (r • v) ↔ ↑r < 0

theorem EuclidGeom.VecND.SameDir.mk0_pos_smul_left {v₁ : EuclidGeom.VecND} {v₂ : EuclidGeom.VecND} (h : EuclidGeom.VecND.SameDir v₁ v₂) {x : ℝ} (hx : 0 < x) : EuclidGeom.VecND.SameDir (Units.mk0 x (_ : x ≠ 0) • v₁) v₂

theorem EuclidGeom.VecND.SameDir.mk0_pos_smul_right {v₁ : EuclidGeom.VecND} {v₂ : EuclidGeom.VecND} (h : EuclidGeom.VecND.SameDir v₁ v₂) {x : ℝ} (hx : 0 < x) : EuclidGeom.VecND.SameDir v₁ (Units.mk0 x (_ : x ≠ 0) • v₂)

theorem EuclidGeom.VecND.SameDir.mk0_neg_smul_left {v₁ : EuclidGeom.VecND} {v₂ : EuclidGeom.VecND} (h : EuclidGeom.VecND.SameDir v₁ v₂) {x : ℝ} (hx : x < 0) : EuclidGeom.VecND.SameDir (Units.mk0 x (_ : x ≠ 0) • v₁) (-v₂)

theorem EuclidGeom.VecND.SameDir.mk0_neg_smul_right {v₁ : EuclidGeom.VecND} {v₂ : EuclidGeom.VecND} (h : EuclidGeom.VecND.SameDir v₁ v₂) {x : ℝ} (hx : x < 0) : EuclidGeom.VecND.SameDir (-v₁) (Units.mk0 x (_ : x ≠ 0) • v₂)

theorem EuclidGeom.VecND.sameDir_comm {v₁ : EuclidGeom.VecND} {v₂ : EuclidGeom.VecND} : EuclidGeom.VecND.SameDir v₁ v₂ ↔ EuclidGeom.VecND.SameDir v₂ v₁

@[simp]

theorem EuclidGeom.VecND.sameDir_map_iff {v₁ : EuclidGeom.VecND} {v₂ : EuclidGeom.VecND} (e : EuclidGeom.Vec ≃ₗ[ℝ] EuclidGeom.Vec) : EuclidGeom.VecND.SameDir ((EuclidGeom.VecND.map e) v₁) ((EuclidGeom.VecND.map e) v₂) ↔ SameRay ℝ ↑v₁ ↑v₂

theorem EuclidGeom.VecND.cdiv_of_sameDir {v₁ : EuclidGeom.VecND} {v₂ : EuclidGeom.VecND} (h : EuclidGeom.VecND.SameDir v₁ v₂) : ↑(v₁ / v₂) = ↑‖v₁‖ / ↑‖v₂‖

theorem EuclidGeom.VecND.angle_of_sameDir {v₁ : EuclidGeom.VecND} {v₂ : EuclidGeom.VecND} {v₃ : EuclidGeom.VecND} {v₄ : EuclidGeom.VecND} (h₁ : EuclidGeom.VecND.SameDir v₁ v₃) (h₂ : EuclidGeom.VecND.SameDir v₂ v₄) : EuclidGeom.VecND.angle v₁ v₂ = EuclidGeom.VecND.angle v₃ v₄

theorem EuclidGeom.VecND.ne_zero_of_ne_zero_smul (v : EuclidGeom.VecND) {t : ℝ} (h : t ≠ 0) : t • ↑v ≠ 0

@[simp]

theorem EuclidGeom.VecND.angle_rotate_right (θ : EuclidGeom.AngValue) (v : EuclidGeom.VecND) : EuclidGeom.VecND.angle v ((EuclidGeom.VecND.rotate θ) v) = θ

@[simp]

theorem EuclidGeom.VecND.sameDir_rotate (θ : EuclidGeom.AngValue) (v₁ : EuclidGeom.VecND) (v₂ : EuclidGeom.VecND) : EuclidGeom.VecND.SameDir ((EuclidGeom.VecND.rotate θ) v₁) ((EuclidGeom.VecND.rotate θ) v₂) ↔ EuclidGeom.VecND.SameDir v₁ v₂

@[simp]

theorem EuclidGeom.VecND.rotate_angle_eq_div_norm_smul (v₁ : EuclidGeom.VecND) (v₂ : EuclidGeom.VecND) : (EuclidGeom.Vec.rotate (EuclidGeom.VecND.angle v₁ v₂)) ↑v₁ = (‖v₁‖ / ‖v₂‖) • ↑v₂

theorem EuclidGeom.VecND.sameDir_rotate_angle_left (v₁ : EuclidGeom.VecND) (v₂ : EuclidGeom.VecND) : EuclidGeom.VecND.SameDir ((EuclidGeom.VecND.rotate (EuclidGeom.VecND.angle v₁ v₂)) v₁) v₂

theorem EuclidGeom.VecND.sameDir_rotate_angle_right (v₁ : EuclidGeom.VecND) (v₂ : EuclidGeom.VecND) : EuclidGeom.VecND.SameDir v₁ ((EuclidGeom.VecND.rotate (EuclidGeom.VecND.angle v₂ v₁)) v₂)

theorem EuclidGeom.VecND.norm_mul_cos (v₁ : EuclidGeom.VecND) (v₂ : EuclidGeom.VecND) : ‖v₁‖ * ‖v₂‖ * EuclidGeom.AngValue.cos (EuclidGeom.VecND.angle v₁ v₂) = inner ↑v₁ ↑v₂

theorem EuclidGeom.VecND.norm_mul_sin (v₁ : EuclidGeom.VecND) (v₂ : EuclidGeom.VecND) : ‖v₁‖ * ‖v₂‖ * EuclidGeom.AngValue.sin (EuclidGeom.VecND.angle v₁ v₂) = (EuclidGeom.Vec.det ↑v₁) ↑v₂

theorem EuclidGeom.VecND.norm_smul_expMapCircle (v₁ : EuclidGeom.VecND) (v₂ : EuclidGeom.VecND) : (‖v₁‖ * ‖v₂‖) • ↑(EuclidGeom.AngValue.expMapCircle (EuclidGeom.VecND.angle v₁ v₂)) = inner ↑v₁ ↑v₂

@[inline, reducible]

abbrev EuclidGeom.Dir : Type

Equations

• EuclidGeom.Dir = Module.Ray ℝ EuclidGeom.Vec

@[inline, reducible]

abbrev EuclidGeom.VecND.toDir (v : EuclidGeom.VecND) : EuclidGeom.Dir

Equations

• v.toDir = ⟦v⟧

@[simp]

theorem EuclidGeom.Dir.quotient_mk_eq (v : EuclidGeom.VecND) : ⟦v⟧ = v.toDir

instance EuclidGeom.instCoeVecNDDir : Coe EuclidGeom.VecND EuclidGeom.Dir

Equations

• EuclidGeom.instCoeVecNDDir = { coe := EuclidGeom.VecND.toDir }

@[simp]

theorem EuclidGeom.VecND.neg_toDir (v : EuclidGeom.VecND) : (-v).toDir = -v.toDir

@[simp]

theorem EuclidGeom.VecND.toDir_eq_toDir_iff {v₁ : EuclidGeom.VecND} {v₂ : EuclidGeom.VecND} : v₁.toDir = v₂.toDir ↔ EuclidGeom.VecND.SameDir v₁ v₂

@[simp]

theorem EuclidGeom.VecND.smul_pos_toDir {x : ℝ} (v : EuclidGeom.VecND) (hx : 0 < x) : (Units.mk0 x (_ : x ≠ 0) • v).toDir = v.toDir

@[simp]

theorem EuclidGeom.VecND.smul_neg_toDir {x : ℝ} (v : EuclidGeom.VecND) (hx : x < 0) : (Units.mk0 x (_ : x ≠ 0) • v).toDir = -v.toDir

theorem EuclidGeom.Dir.ind {C : EuclidGeom.Dir → Prop} (h : ∀ (v : EuclidGeom.VecND), C v.toDir) (x : EuclidGeom.Dir) : C x

def EuclidGeom.Dir.map (f : EuclidGeom.Vec ≃ₗ[ℝ] EuclidGeom.Vec) : EuclidGeom.Dir ≃ EuclidGeom.Dir

Equations

• EuclidGeom.Dir.map f = Module.Ray.map f

@[simp]

theorem EuclidGeom.Dir.map_apply (f : EuclidGeom.Vec ≃ₗ[ℝ] EuclidGeom.Vec) (v : EuclidGeom.VecND) : (EuclidGeom.Dir.map f) v.toDir = { val := f ↑v, property := (_ : f ↑v ≠ 0) }.toDir

@[simp]

theorem EuclidGeom.Dir.map_refl : EuclidGeom.Dir.map (LinearEquiv.refl ℝ EuclidGeom.Vec) = Equiv.refl EuclidGeom.Dir

@[simp]

theorem EuclidGeom.Dir.map_symm (f : EuclidGeom.Vec ≃ₗ[ℝ] EuclidGeom.Vec) : (EuclidGeom.Dir.map f).symm = EuclidGeom.Dir.map (LinearEquiv.symm f)

@[simp]

theorem EuclidGeom.Dir.map_trans (f₁ : EuclidGeom.Vec ≃ₗ[ℝ] EuclidGeom.Vec) (f₂ : EuclidGeom.Vec ≃ₗ[ℝ] EuclidGeom.Vec) : EuclidGeom.Dir.map (f₁ ≪≫ₗ f₂) = (EuclidGeom.Dir.map f₁).trans (EuclidGeom.Dir.map f₂)

class EuclidGeom.Dir.NegCommute {α : Type u_1} [Neg α] (f : EuclidGeom.Dir → α) : Prop

• map_neg' : ∀ (d : EuclidGeom.Dir), f (-d) = -f d

theorem EuclidGeom.Dir.map_neg {α : Type u_1} [Neg α] (f : EuclidGeom.Dir → α) [EuclidGeom.Dir.NegCommute f] (d : EuclidGeom.Dir) : f (-d) = -f d

@[simp]

theorem EuclidGeom.Dir.map_neg' (f : EuclidGeom.Dir ≃ EuclidGeom.Dir) [EuclidGeom.Dir.NegCommute ⇑f] (d : EuclidGeom.Dir) : f (-d) = -f d

instance EuclidGeom.Dir.negCommute_refl : EuclidGeom.Dir.NegCommute ⇑(Equiv.refl EuclidGeom.Dir)

Equations

• EuclidGeom.Dir.negCommute_refl = (_ : EuclidGeom.Dir.NegCommute ⇑(Equiv.refl EuclidGeom.Dir))

instance EuclidGeom.Dir.negCommute_symm (f : EuclidGeom.Dir ≃ EuclidGeom.Dir) [EuclidGeom.Dir.NegCommute ⇑f] : EuclidGeom.Dir.NegCommute ⇑f.symm

Equations

• (_ : EuclidGeom.Dir.NegCommute ⇑f.symm) = (_ : EuclidGeom.Dir.NegCommute ⇑f.symm)

instance EuclidGeom.Dir.negCommute_comp {α : Type u_1} [Neg α] (f : EuclidGeom.Dir → EuclidGeom.Dir) (g : EuclidGeom.Dir → α) [EuclidGeom.Dir.NegCommute f] [EuclidGeom.Dir.NegCommute g] : EuclidGeom.Dir.NegCommute (g ∘ f)

Equations

• (_ : EuclidGeom.Dir.NegCommute (g ∘ f)) = (_ : EuclidGeom.Dir.NegCommute (g ∘ f))

instance EuclidGeom.Dir.negCommute_trans (f : EuclidGeom.Dir ≃ EuclidGeom.Dir) (g : EuclidGeom.Dir ≃ EuclidGeom.Dir) [EuclidGeom.Dir.NegCommute ⇑f] [EuclidGeom.Dir.NegCommute ⇑g] : EuclidGeom.Dir.NegCommute ⇑(f.trans g)

Equations

• (_ : EuclidGeom.Dir.NegCommute ⇑(f.trans g)) = (_ : EuclidGeom.Dir.NegCommute (⇑g ∘ ⇑f))

instance EuclidGeom.Dir.negCommute_map (f : EuclidGeom.Vec ≃ₗ[ℝ] EuclidGeom.Vec) : EuclidGeom.Dir.NegCommute ⇑(EuclidGeom.Dir.map f)

Equations

• (_ : EuclidGeom.Dir.NegCommute ⇑(EuclidGeom.Dir.map f)) = (_ : EuclidGeom.Dir.NegCommute ⇑(EuclidGeom.Dir.map f))

@[inline, reducible]

abbrev EuclidGeom.Dir.rotate (θ : EuclidGeom.AngValue) : EuclidGeom.Dir ≃ EuclidGeom.Dir

Equations

• EuclidGeom.Dir.rotate θ = EuclidGeom.Dir.map (LinearEquiv.restrictScalars ℝ (EuclidGeom.Vec.rotate θ))

instance EuclidGeom.Dir.negCommute_rotate (θ : EuclidGeom.AngValue) : EuclidGeom.Dir.NegCommute ⇑(EuclidGeom.Dir.rotate θ)

Equations

• (_ : EuclidGeom.Dir.NegCommute ⇑(EuclidGeom.Dir.rotate θ)) = (_ : EuclidGeom.Dir.NegCommute ⇑(EuclidGeom.Dir.map (LinearEquiv.restrictScalars ℝ (EuclidGeom.Vec.rotate θ))))

@[simp]

theorem EuclidGeom.Dir.rotate_zero : EuclidGeom.Dir.rotate 0 = Equiv.refl EuclidGeom.Dir

theorem EuclidGeom.Dir.rotate_pi_apply (d : EuclidGeom.Dir) : (EuclidGeom.Dir.rotate ∠[Real.pi]) d = -d

theorem EuclidGeom.Dir.rotate_add_apply (θ : EuclidGeom.AngValue) (ψ : EuclidGeom.AngValue) (d : EuclidGeom.Dir) : (EuclidGeom.Dir.rotate (θ + ψ)) d = (EuclidGeom.Dir.rotate θ) ((EuclidGeom.Dir.rotate ψ) d)

theorem EuclidGeom.Dir.rotate_add (θ : EuclidGeom.AngValue) (ψ : EuclidGeom.AngValue) : EuclidGeom.Dir.rotate (θ + ψ) = EuclidGeom.Dir.rotate θ * EuclidGeom.Dir.rotate ψ

instance EuclidGeom.Dir.instVAddAngValueDir : VAdd EuclidGeom.AngValue EuclidGeom.Dir

Equations

• EuclidGeom.Dir.instVAddAngValueDir = { vadd := fun (θ : EuclidGeom.AngValue) => ⇑(EuclidGeom.Dir.rotate θ) }

theorem EuclidGeom.Dir.vadd_def (θ : EuclidGeom.AngValue) (p : EuclidGeom.Dir) : θ +ᵥ p = (EuclidGeom.Dir.map (LinearEquiv.restrictScalars ℝ (EuclidGeom.Vec.rotate θ))) p

instance EuclidGeom.Dir.instNonemptyDir : Nonempty EuclidGeom.Dir

Equations

• EuclidGeom.Dir.instNonemptyDir = (_ : Nonempty (Quotient (RayVector.Setoid ℝ EuclidGeom.Vec)))

instance EuclidGeom.Dir.instAddTorsorAngValueDirToAddGroupToNormedAddGroupInstNormedAddCommGroupAngValue : AddTorsor EuclidGeom.AngValue EuclidGeom.Dir

Equations

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

@[simp]

theorem EuclidGeom.Dir.rotate_eq_vadd (θ : EuclidGeom.AngValue) (d : EuclidGeom.Dir) : (EuclidGeom.Dir.rotate θ) d = θ +ᵥ d

@[simp]

theorem EuclidGeom.Dir.vsub_toDir (v₁ : EuclidGeom.VecND) (v₂ : EuclidGeom.VecND) : v₂.toDir -ᵥ v₁.toDir = EuclidGeom.VecND.angle v₁ v₂

@[simp]

theorem EuclidGeom.Dir.vadd_neg (θ : EuclidGeom.AngValue) (d : EuclidGeom.Dir) : θ +ᵥ -d = -(θ +ᵥ d)

@[simp]

theorem EuclidGeom.Dir.pi_vadd (d : EuclidGeom.Dir) : ∠[Real.pi] +ᵥ d = -d

@[simp]

theorem EuclidGeom.Dir.neg_vsub_left (d₁ : EuclidGeom.Dir) (d₂ : EuclidGeom.Dir) : -d₁ -ᵥ d₂ = d₁ -ᵥ d₂ + ∠[Real.pi]

@[simp]

theorem EuclidGeom.Dir.neg_vsub_right (d₁ : EuclidGeom.Dir) (d₂ : EuclidGeom.Dir) : d₁ -ᵥ -d₂ = d₁ -ᵥ d₂ + ∠[Real.pi]

theorem EuclidGeom.Dir.eq_neg_of_vsub_eq_pi (d₁ : EuclidGeom.Dir) (d₂ : EuclidGeom.Dir) : d₁ = -d₂ ↔ d₁ -ᵥ d₂ = ∠[Real.pi]

@[inline, reducible]

abbrev EuclidGeom.Dir.normalize {M : Type u_1} [AddCommGroup M] [Module ℝ M] {F : Type u_2} [LinearMapClass F ℝ EuclidGeom.Vec M] (f : F) : EuclidGeom.Dir → M

Equations

• EuclidGeom.Dir.normalize f = Quotient.lift (fun (v : EuclidGeom.VecND) => ‖v‖⁻¹ • f ↑v) (_ : ∀ (x y : RayVector ℝ EuclidGeom.Vec), x ≈ y → ‖↑x‖⁻¹ • f ↑x = ‖↑y‖⁻¹ • f ↑y)

@[simp]

theorem EuclidGeom.Dir.normalize_apply {M : Type u_1} [AddCommGroup M] [Module ℝ M] {F : Type u_2} [LinearMapClass F ℝ EuclidGeom.Vec M] (f : F) (v : EuclidGeom.VecND) : EuclidGeom.Dir.normalize f ⟦v⟧ = ‖v‖⁻¹ • f ↑v

theorem EuclidGeom.Dir.normalize_apply_ne_zero {M : Type u_1} [AddCommGroup M] [Module ℝ M] {F : Type u_2} [LinearMapClass F ℝ EuclidGeom.Vec M] (f : F) (hf : Function.Injective ⇑f) (d : EuclidGeom.Dir) : EuclidGeom.Dir.normalize f d ≠ 0

def EuclidGeom.Dir.unitVecND (d : EuclidGeom.Dir) : EuclidGeom.VecND

Equations

• d.unitVecND = { val := EuclidGeom.Dir.normalize LinearMap.id d, property := (_ : EuclidGeom.Dir.normalize LinearMap.id d ≠ 0) }

@[inline, reducible]

abbrev EuclidGeom.Dir.unitVec (d : EuclidGeom.Dir) : EuclidGeom.Vec

Equations

• d.unitVec = ↑d.unitVecND

@[simp]

theorem EuclidGeom.Dir.coe_unitVecND (d : EuclidGeom.Dir) : ↑d.unitVecND = d.unitVec

theorem EuclidGeom.VecND.toDir_unitVecND (v : EuclidGeom.VecND) : v.toDir.unitVecND = { val := ‖v‖⁻¹ • ↑v, property := (_ : ¬‖v‖⁻¹ • ↑v = 0) }

theorem EuclidGeom.VecND.toDir_unitVec (v : EuclidGeom.VecND) : v.toDir.unitVec = ‖v‖⁻¹ • ↑v

theorem EuclidGeom.VecND.inv_norm_smul (v : EuclidGeom.VecND) : ‖v‖⁻¹ • ↑v = ↑v.toDir.unitVecND

@[simp]

theorem EuclidGeom.Dir.neg_unitVecND (d : EuclidGeom.Dir) : (-d).unitVecND = -d.unitVecND

@[simp]

theorem EuclidGeom.Dir.neg_unitVec (d : EuclidGeom.Dir) : (-d).unitVec = -d.unitVec

@[simp]

theorem EuclidGeom.VecND.norm_smul_toDir_unitVec (v : EuclidGeom.VecND) : ‖v‖ • v.toDir.unitVec = ↑v

@[simp]

theorem EuclidGeom.Vec.norm_smul_toDir_unitVec {v : EuclidGeom.Vec} (hv : v ≠ 0) : ‖v‖ • (EuclidGeom.VecND.mk v hv).toDir.unitVec = v

@[simp]

theorem EuclidGeom.Dir.unitVecND_toDir (d : EuclidGeom.Dir) : d.unitVecND.toDir = d

theorem EuclidGeom.Dir.norm_unitVec (d : EuclidGeom.Dir) : ‖d.unitVec‖ = 1

@[simp]

theorem EuclidGeom.Dir.norm_unitVecND (d : EuclidGeom.Dir) : ‖d.unitVecND‖ = 1

instance EuclidGeom.Dir.instCircularOrderedAddTorsor : CircularOrderedAddTorsor EuclidGeom.AngValue EuclidGeom.Dir

Equations

• EuclidGeom.Dir.instCircularOrderedAddTorsor = AddTorsor.CircularOrderedAddTorsor_of_CircularOrderedAddCommGroup EuclidGeom.AngValue EuclidGeom.Dir

theorem EuclidGeom.Dir.btw_def₁ {d₁ : EuclidGeom.Dir} {d₂ : EuclidGeom.Dir} {d₃ : EuclidGeom.Dir} : btw d₁ d₂ d₃ ↔ btw 0 (d₂ -ᵥ d₁) (d₃ -ᵥ d₁)

theorem EuclidGeom.Dir.btw_def₂ {d₁ : EuclidGeom.Dir} {d₂ : EuclidGeom.Dir} {d₃ : EuclidGeom.Dir} : btw d₁ d₂ d₃ ↔ btw (d₁ -ᵥ d₂) 0 (d₃ -ᵥ d₂)

theorem EuclidGeom.Dir.btw_def₃ {d₁ : EuclidGeom.Dir} {d₂ : EuclidGeom.Dir} {d₃ : EuclidGeom.Dir} : btw d₁ d₂ d₃ ↔ btw (d₁ -ᵥ d₃) (d₂ -ᵥ d₃) 0

theorem EuclidGeom.Dir.btw_iff_btw_vsub {d₁ : EuclidGeom.Dir} {d₂ : EuclidGeom.Dir} {d₃ : EuclidGeom.Dir} (d : EuclidGeom.Dir) : btw d₁ d₂ d₃ ↔ btw (d₁ -ᵥ d) (d₂ -ᵥ d) (d₃ -ᵥ d)

theorem EuclidGeom.Dir.sbtw_def₁ {d₁ : EuclidGeom.Dir} {d₂ : EuclidGeom.Dir} {d₃ : EuclidGeom.Dir} : sbtw d₁ d₂ d₃ ↔ sbtw 0 (d₂ -ᵥ d₁) (d₃ -ᵥ d₁)

theorem EuclidGeom.Dir.sbtw_def₂ {d₁ : EuclidGeom.Dir} {d₂ : EuclidGeom.Dir} {d₃ : EuclidGeom.Dir} : sbtw d₁ d₂ d₃ ↔ sbtw (d₁ -ᵥ d₂) 0 (d₃ -ᵥ d₂)

theorem EuclidGeom.Dir.sbtw_def₃ {d₁ : EuclidGeom.Dir} {d₂ : EuclidGeom.Dir} {d₃ : EuclidGeom.Dir} : sbtw d₁ d₂ d₃ ↔ sbtw (d₁ -ᵥ d₃) (d₂ -ᵥ d₃) 0

theorem EuclidGeom.Dir.sbtw_iff_sbtw_vsub {d₁ : EuclidGeom.Dir} {d₂ : EuclidGeom.Dir} {d₃ : EuclidGeom.Dir} (d : EuclidGeom.Dir) : sbtw d₁ d₂ d₃ ↔ sbtw (d₁ -ᵥ d) (d₂ -ᵥ d) (d₃ -ᵥ d)

@[simp]

theorem EuclidGeom.Dir.btw_neg {d₁ : EuclidGeom.Dir} {d₂ : EuclidGeom.Dir} {d₃ : EuclidGeom.Dir} : btw (-d₁) (-d₂) (-d₃) ↔ btw d₁ d₂ d₃

@[simp]

theorem EuclidGeom.Dir.sbtw_neg {d₁ : EuclidGeom.Dir} {d₂ : EuclidGeom.Dir} {d₃ : EuclidGeom.Dir} : sbtw (-d₁) (-d₂) (-d₃) ↔ sbtw d₁ d₂ d₃

@[simp]

theorem EuclidGeom.angle_toDir_unitVecND_left (v₁ : EuclidGeom.VecND) (v₂ : EuclidGeom.VecND) : EuclidGeom.VecND.angle v₁.toDir.unitVecND v₂ = EuclidGeom.VecND.angle v₁ v₂

@[simp]

theorem EuclidGeom.angle_toDir_unitVecND_right (v₁ : EuclidGeom.VecND) (v₂ : EuclidGeom.VecND) : EuclidGeom.VecND.angle v₁ v₂.toDir.unitVecND = EuclidGeom.VecND.angle v₁ v₂

@[simp]

theorem EuclidGeom.Dir.angle_unitVecND (d₁ : EuclidGeom.Dir) (d₂ : EuclidGeom.Dir) : EuclidGeom.VecND.angle d₁.unitVecND d₂.unitVecND = d₂ -ᵥ d₁

@[simp]

theorem EuclidGeom.Dir.inner_unitVec (d₁ : EuclidGeom.Dir) (d₂ : EuclidGeom.Dir) : inner d₁.unitVec d₂.unitVec = EuclidGeom.AngValue.cos (d₂ -ᵥ d₁)

@[simp]

theorem EuclidGeom.Dir.det_unitVec (d₁ : EuclidGeom.Dir) (d₂ : EuclidGeom.Dir) : (EuclidGeom.Vec.det d₁.unitVec) d₂.unitVec = EuclidGeom.AngValue.sin (d₂ -ᵥ d₁)

theorem EuclidGeom.Dir.complex_inner_unitVec (d₁ : EuclidGeom.Dir) (d₂ : EuclidGeom.Dir) : inner d₁.unitVec d₂.unitVec = ↑(EuclidGeom.AngValue.expMapCircle (d₂ -ᵥ d₁))

def EuclidGeom.Proj : Type

Equations

• EuclidGeom.Proj = Quotient ((Setoid.correspondence (RayVector.Setoid ℝ EuclidGeom.Vec)) { val := projectivizationSetoid ℝ EuclidGeom.Vec, property := EuclidGeom.Proj.proof_1 })

def EuclidGeom.Dir.toProj : EuclidGeom.Dir → EuclidGeom.Proj

Equations

• EuclidGeom.Dir.toProj = Quotient.mk ((Setoid.correspondence (RayVector.Setoid ℝ EuclidGeom.Vec)) { val := projectivizationSetoid ℝ EuclidGeom.Vec, property := EuclidGeom.Proj.proof_1 })

@[inline, reducible]

abbrev EuclidGeom.VecND.toProj (v : EuclidGeom.VecND) : EuclidGeom.Proj

Equations

• v.toProj = v.toDir.toProj

@[simp]

theorem EuclidGeom.Dir.unitVecND_toProj (d : EuclidGeom.Dir) : d.unitVecND.toProj = d.toProj

theorem EuclidGeom.VecND.toProj_eq_toProj_iff₀ {v₁ : EuclidGeom.VecND} {v₂ : EuclidGeom.VecND} : v₁.toProj = v₂.toProj ↔ ∃ (a : ℝˣ), ↑v₁ = a • ↑v₂

theorem EuclidGeom.VecND.toProj_eq_toProj_iff {v₁ : EuclidGeom.VecND} {v₂ : EuclidGeom.VecND} : v₁.toProj = v₂.toProj ↔ ∃ (a : ℝ), ↑v₁ = a • ↑v₂

theorem EuclidGeom.VecND.toProj_eq_toProj_iff' {v₁ : EuclidGeom.VecND} {v₂ : EuclidGeom.VecND} : v₁.toProj = v₂.toProj ↔ ∃ (a : ℝˣ), v₁ = a • v₂

instance EuclidGeom.instCoeDirProj : Coe EuclidGeom.Dir EuclidGeom.Proj

Equations

• EuclidGeom.instCoeDirProj = { coe := fun (v : EuclidGeom.Dir) => v.toProj }

@[simp]

theorem EuclidGeom.VecND.toDir_toProj (v : EuclidGeom.VecND) : v.toDir.toProj = v.toProj

theorem EuclidGeom.Dir.toProj_eq_toProj_iff {d₁ : EuclidGeom.Dir} {d₂ : EuclidGeom.Dir} : d₁.toProj = d₂.toProj ↔ d₁ = d₂ ∨ d₁ = -d₂

theorem EuclidGeom.Dir.toProj_eq_of_eq {d₁ : EuclidGeom.Dir} {d₂ : EuclidGeom.Dir} (h : d₁ = d₂) : d₁.toProj = d₂.toProj

theorem EuclidGeom.Dir.toProj_eq_of_eq_neg {d₁ : EuclidGeom.Dir} {d₂ : EuclidGeom.Dir} (h : d₁ = -d₂) : d₁.toProj = d₂.toProj

theorem EuclidGeom.Dir.toProj_eq_toProj_iff_unitVec₀ {d₁ : EuclidGeom.Dir} {d₂ : EuclidGeom.Dir} : d₁.toProj = d₂.toProj ↔ ∃ (a : ℝˣ), d₁.unitVec = a • d₂.unitVec

theorem EuclidGeom.Dir.toProj_eq_toProj_iff_unitVec {d₁ : EuclidGeom.Dir} {d₂ : EuclidGeom.Dir} : d₁.toProj = d₂.toProj ↔ ∃ (a : ℝ), d₁.unitVec = a • d₂.unitVec

theorem EuclidGeom.Dir.toProj_eq_toProj_iff_unitVecND {d₁ : EuclidGeom.Dir} {d₂ : EuclidGeom.Dir} : d₁.toProj = d₂.toProj ↔ ∃ (a : ℝˣ), d₁.unitVecND = a • d₂.unitVecND

theorem EuclidGeom.Dir.toProj_eq_toProj_iff_vsub_not_isND {d₁ : EuclidGeom.Dir} {d₂ : EuclidGeom.Dir} : d₁.toProj = d₂.toProj ↔ ¬(d₁ -ᵥ d₂).IsND

theorem EuclidGeom.Dir.toProj_ne_toProj_iff_vsub_isND {d₁ : EuclidGeom.Dir} {d₂ : EuclidGeom.Dir} : d₁.toProj ≠ d₂.toProj ↔ (d₁ -ᵥ d₂).IsND

theorem EuclidGeom.Dir.toProj_ne_toProj_iff_neg_vsub_isND {d₁ : EuclidGeom.Dir} {d₂ : EuclidGeom.Dir} : d₁.toProj ≠ d₂.toProj ↔ (d₂ -ᵥ d₁).IsND

theorem EuclidGeom.Dir.toProj_eq_toProj_iff_neg_vsub_not_isND {d₁ : EuclidGeom.Dir} {d₂ : EuclidGeom.Dir} : d₁.toProj = d₂.toProj ↔ ¬(d₂ -ᵥ d₁).IsND

@[simp]

theorem EuclidGeom.VecND.neg_toProj (v : EuclidGeom.VecND) : (-v).toProj = v.toProj

@[simp]

theorem EuclidGeom.Dir.toProj_neg (d : EuclidGeom.Dir) : (-d).toProj = d.toProj

theorem EuclidGeom.Vec.det_eq_zero_iff_eq_smul_right {u : EuclidGeom.Vec} {v : EuclidGeom.Vec} : (EuclidGeom.Vec.det u) v = 0 ↔ v = 0 ∨ ∃ (t : ℝ), u = t • v

theorem EuclidGeom.Vec.det_eq_zero_iff_eq_smul_left {u : EuclidGeom.Vec} {v : EuclidGeom.Vec} : (EuclidGeom.Vec.det u) v = 0 ↔ u = 0 ∨ ∃ (t : ℝ), v = t • u

theorem EuclidGeom.VecND.det_eq_zero_iff_toProj_eq_toProj {u : EuclidGeom.VecND} {v : EuclidGeom.VecND} : (EuclidGeom.Vec.det ↑u) ↑v = 0 ↔ u.toProj = v.toProj

theorem EuclidGeom.Proj.ind {C : EuclidGeom.Proj → Prop} (h : ∀ (d : EuclidGeom.Dir), C d.toProj) (x : EuclidGeom.Proj) : C x

@[inline, reducible]

abbrev EuclidGeom.Proj.lift {α : Sort u_1} (f : EuclidGeom.Dir → α) (hf : ∀ (d : EuclidGeom.Dir), f (-d) = f d) : EuclidGeom.Proj → α

Equations

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

@[simp]

theorem EuclidGeom.Proj.lift_dir_toProj {α : Sort u_1} (f : EuclidGeom.Dir → α) (hf : ∀ (d : EuclidGeom.Dir), f (-d) = f d) (d : EuclidGeom.Dir) : EuclidGeom.Proj.lift f hf d.toProj = f d

@[simp]

theorem EuclidGeom.Proj.lift_vecND_toProj {α : Sort u_1} (f : EuclidGeom.Dir → α) (hf : ∀ (d : EuclidGeom.Dir), f (-d) = f d) (v : EuclidGeom.VecND) : EuclidGeom.Proj.lift f hf v.toProj = f v.toDir

def EuclidGeom.Proj.map (f : EuclidGeom.Dir ≃ EuclidGeom.Dir) [EuclidGeom.Dir.NegCommute ⇑f] : EuclidGeom.Proj ≃ EuclidGeom.Proj

Equations

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

@[simp]

theorem EuclidGeom.Proj.map_apply (f : EuclidGeom.Dir ≃ EuclidGeom.Dir) : ∀ {x : EuclidGeom.Dir.NegCommute ⇑f} (d : EuclidGeom.Dir), (EuclidGeom.Proj.map f) d.toProj = (f d).toProj

@[simp]

theorem EuclidGeom.Proj.map_vecND_toProj (f : EuclidGeom.Dir ≃ EuclidGeom.Dir) : ∀ {x : EuclidGeom.Dir.NegCommute ⇑f} (v : EuclidGeom.VecND), (EuclidGeom.Proj.map f) v.toProj = (f v.toDir).toProj

@[simp]

theorem EuclidGeom.Proj.map_refl : EuclidGeom.Proj.map (Equiv.refl EuclidGeom.Dir) = Equiv.refl EuclidGeom.Proj

@[simp]

theorem EuclidGeom.Proj.map_symm (f : EuclidGeom.Dir ≃ EuclidGeom.Dir) : ∀ {x : EuclidGeom.Dir.NegCommute ⇑f}, (EuclidGeom.Proj.map f).symm = EuclidGeom.Proj.map f.symm

@[simp]

theorem EuclidGeom.Proj.map_trans (f : EuclidGeom.Dir ≃ EuclidGeom.Dir) (g : EuclidGeom.Dir ≃ EuclidGeom.Dir) : ∀ {x : EuclidGeom.Dir.NegCommute ⇑f} {x_1 : EuclidGeom.Dir.NegCommute ⇑g}, EuclidGeom.Proj.map (f.trans g) = (EuclidGeom.Proj.map f).trans (EuclidGeom.Proj.map g)

instance EuclidGeom.Proj.instNonemptyProj : Nonempty EuclidGeom.Proj

Equations

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

instance EuclidGeom.Proj.instVAddAngDValueProj : VAdd EuclidGeom.AngDValue EuclidGeom.Proj

Equations

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

theorem EuclidGeom.Proj.vadd_coe_left (θ : EuclidGeom.AngValue) (p : EuclidGeom.Proj) : ↑θ +ᵥ p = (EuclidGeom.Proj.map (EuclidGeom.Dir.rotate θ)) p

@[simp]

theorem EuclidGeom.Proj.vadd_coe (θ : EuclidGeom.AngValue) (d : EuclidGeom.Dir) : ↑θ +ᵥ d.toProj = (θ +ᵥ d).toProj

instance EuclidGeom.Proj.instAddTorsorAngDValueProjToAddGroupToNormedAddGroupInstNormedAddCommGroupAngDValue : AddTorsor EuclidGeom.AngDValue EuclidGeom.Proj

Equations

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

instance EuclidGeom.Proj.instCircularOrderedAddTorsor : CircularOrderedAddTorsor EuclidGeom.AngDValue EuclidGeom.Proj

Equations

• EuclidGeom.Proj.instCircularOrderedAddTorsor = AddTorsor.CircularOrderedAddTorsor_of_CircularOrderedAddCommGroup EuclidGeom.AngDValue EuclidGeom.Proj

def EuclidGeom.Proj.perp (p : EuclidGeom.Proj) : EuclidGeom.Proj

Equations

• p.perp = ↑∠[Real.pi / 2] +ᵥ p

@[simp]

theorem EuclidGeom.Proj.perp_perp (p : EuclidGeom.Proj) : p.perp.perp = p