Theorems · Theorem · linear algebra

LinearMap.span_singleton_inf_orthogonal_eq_bot

∀ {K : Type u_7} {K₁ : Type u_8} {V₁ : Type u_10} {V₂ : Type u_11} [inst : Field K] [inst_1 : Field K₁]
  [inst_2 : AddCommGroup V₁] [inst_3 : Module K₁ V₁] [inst_4 : AddCommGroup V₂] [inst_5 : Module K V₂]
  {J₁ J₁' : K₁ →+* K} (B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂) (x : V₁),
  (B x) x ≠ 0 → K₁ ∙ x ⊓ Submodule.orthogonalBilin B (K₁ ∙ x) = ⊥

Defined in

Mathlib.LinearAlgebra.SesquilinearForm.Orthogonal

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldFieldAddCommGroupModuleAddCommGroupModule