R : Type u_1
R₁ : Type ?u.588000
R₂ : Type ?u.588003
R₃ : Type ?u.588006
M : Type u_2
M₁ : Type ?u.588012
M₂ : Type ?u.588015
Mₗ₁ : Type ?u.588018
Mₗ₁' : Type ?u.588021
Mₗ₂ : Type ?u.588024
Mₗ₂' : Type ?u.588027
K : Type ?u.588030
K₁ : Type ?u.588033
K₂ : Type ?u.588036
V : Type ?u.588039
V₁ : Type ?u.588042
V₂ : Type ?u.588045
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] R
v : Basis n R M
h : IsOrthoᵢ B ↑v
hB : SeparatingLeft B
i : n
ho : IsOrtho B (↑v i) (↑v i)
⊢ False
R : Type u_1
R₁ : Type ?u.588000
R₂ : Type ?u.588003
R₃ : Type ?u.588006
M : Type u_2
M₁ : Type ?u.588012
M₂ : Type ?u.588015
Mₗ₁ : Type ?u.588018
Mₗ₁' : Type ?u.588021
Mₗ₂ : Type ?u.588024
Mₗ₂' : Type ?u.588027
K : Type ?u.588030
K₁ : Type ?u.588033
K₂ : Type ?u.588036
V : Type ?u.588039
V₁ : Type ?u.588042
V₂ : Type ?u.588045
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] R
v : Basis n R M
h : IsOrthoᵢ B ↑v
hB : SeparatingLeft B
i : n
⊢ ¬IsOrtho B (↑v i) (↑v i)
intro ho
R : Type u_1
R₁ : Type ?u.588000
R₂ : Type ?u.588003
R₃ : Type ?u.588006
M : Type u_2
M₁ : Type ?u.588012
M₂ : Type ?u.588015
Mₗ₁ : Type ?u.588018
Mₗ₁' : Type ?u.588021
Mₗ₂ : Type ?u.588024
Mₗ₂' : Type ?u.588027
K : Type ?u.588030
K₁ : Type ?u.588033
K₂ : Type ?u.588036
V : Type ?u.588039
V₁ : Type ?u.588042
V₂ : Type ?u.588045
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] R
v : Basis n R M
h : IsOrthoᵢ B ↑v
hB : SeparatingLeft B
i : n
ho : IsOrtho B (↑v i) (↑v i)
m : M
⊢ ↑(↑B (↑v i)) m = 0
R : Type u_1
R₁ : Type ?u.588000
R₂ : Type ?u.588003
R₃ : Type ?u.588006
M : Type u_2
M₁ : Type ?u.588012
M₂ : Type ?u.588015
Mₗ₁ : Type ?u.588018
Mₗ₁' : Type ?u.588021
Mₗ₂ : Type ?u.588024
Mₗ₂' : Type ?u.588027
K : Type ?u.588030
K₁ : Type ?u.588033
K₂ : Type ?u.588036
V : Type ?u.588039
V₁ : Type ?u.588042
V₂ : Type ?u.588045
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] R
v : Basis n R M
h : IsOrthoᵢ B ↑v
hB : SeparatingLeft B
i : n
ho : IsOrtho B (↑v i) (↑v i)
⊢ False
refine' v.ne_zero i (hB (v i) fun m ↦ _)
case intro
R : Type u_1
R₁ : Type ?u.588000
R₂ : Type ?u.588003
R₃ : Type ?u.588006
M : Type u_2
M₁ : Type ?u.588012
M₂ : Type ?u.588015
Mₗ₁ : Type ?u.588018
Mₗ₁' : Type ?u.588021
Mₗ₂ : Type ?u.588024
Mₗ₂' : Type ?u.588027
K : Type ?u.588030
K₁ : Type ?u.588033
K₂ : Type ?u.588036
V : Type ?u.588039
V₁ : Type ?u.588042
V₂ : Type ?u.588045
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] R
v : Basis n R M
h : IsOrthoᵢ B ↑v
hB : SeparatingLeft B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
⊢ ↑(↑B (↑v i)) (↑(LinearEquiv.symm v.repr) vi) = 0
R : Type u_1
R₁ : Type ?u.588000
R₂ : Type ?u.588003
R₃ : Type ?u.588006
M : Type u_2
M₁ : Type ?u.588012
M₂ : Type ?u.588015
Mₗ₁ : Type ?u.588018
Mₗ₁' : Type ?u.588021
Mₗ₂ : Type ?u.588024
Mₗ₂' : Type ?u.588027
K : Type ?u.588030
K₁ : Type ?u.588033
K₂ : Type ?u.588036
V : Type ?u.588039
V₁ : Type ?u.588042
V₂ : Type ?u.588045
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] R
v : Basis n R M
h : IsOrthoᵢ B ↑v
hB : SeparatingLeft B
i : n
ho : IsOrtho B (↑v i) (↑v i)
m : M
⊢ ↑(↑B (↑v i)) m = 0
obtain ⟨vi, rfl⟩ := v.repr.symm.surjective m
case intro
R : Type u_1
R₁ : Type ?u.588000
R₂ : Type ?u.588003
R₃ : Type ?u.588006
M : Type u_2
M₁ : Type ?u.588012
M₂ : Type ?u.588015
Mₗ₁ : Type ?u.588018
Mₗ₁' : Type ?u.588021
Mₗ₂ : Type ?u.588024
Mₗ₂' : Type ?u.588027
K : Type ?u.588030
K₁ : Type ?u.588033
K₂ : Type ?u.588036
V : Type ?u.588039
V₁ : Type ?u.588042
V₂ : Type ?u.588045
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] R
v : Basis n R M
h : IsOrthoᵢ B ↑v
hB : SeparatingLeft B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
⊢ ∑ i_1 in vi.support, ↑(↑B (↑v i)) (↑vi i_1 • ↑v i_1) = 0
case intro
R : Type u_1
R₁ : Type ?u.588000
R₂ : Type ?u.588003
R₃ : Type ?u.588006
M : Type u_2
M₁ : Type ?u.588012
M₂ : Type ?u.588015
Mₗ₁ : Type ?u.588018
Mₗ₁' : Type ?u.588021
Mₗ₂ : Type ?u.588024
Mₗ₂' : Type ?u.588027
K : Type ?u.588030
K₁ : Type ?u.588033
K₂ : Type ?u.588036
V : Type ?u.588039
V₁ : Type ?u.588042
V₂ : Type ?u.588045
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] R
v : Basis n R M
h : IsOrthoᵢ B ↑v
hB : SeparatingLeft B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
⊢ ↑(↑B (↑v i)) (↑(LinearEquiv.symm v.repr) vi) = 0
rw [Basis.repr_symm_apply, Finsupp.total_apply, Finsupp.sum, map_sum]
case intro.h
R : Type u_1
R₁ : Type ?u.588000
R₂ : Type ?u.588003
R₃ : Type ?u.588006
M : Type u_2
M₁ : Type ?u.588012
M₂ : Type ?u.588015
Mₗ₁ : Type ?u.588018
Mₗ₁' : Type ?u.588021
Mₗ₂ : Type ?u.588024
Mₗ₂' : Type ?u.588027
K : Type ?u.588030
K₁ : Type ?u.588033
K₂ : Type ?u.588036
V : Type ?u.588039
V₁ : Type ?u.588042
V₂ : Type ?u.588045
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] R
v : Basis n R M
h : IsOrthoᵢ B ↑v
hB : SeparatingLeft B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
⊢ ∀ (x : n), x ∈ vi.support → ↑(↑B (↑v i)) (↑vi x • ↑v x) = 0
case intro
R : Type u_1
R₁ : Type ?u.588000
R₂ : Type ?u.588003
R₃ : Type ?u.588006
M : Type u_2
M₁ : Type ?u.588012
M₂ : Type ?u.588015
Mₗ₁ : Type ?u.588018
Mₗ₁' : Type ?u.588021
Mₗ₂ : Type ?u.588024
Mₗ₂' : Type ?u.588027
K : Type ?u.588030
K₁ : Type ?u.588033
K₂ : Type ?u.588036
V : Type ?u.588039
V₁ : Type ?u.588042
V₂ : Type ?u.588045
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] R
v : Basis n R M
h : IsOrthoᵢ B ↑v
hB : SeparatingLeft B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
⊢ ∑ i_1 in vi.support, ↑(↑B (↑v i)) (↑vi i_1 • ↑v i_1) = 0
apply Finset.sum_eq_zero
case intro.h
R : Type u_1
R₁ : Type ?u.588000
R₂ : Type ?u.588003
R₃ : Type ?u.588006
M : Type u_2
M₁ : Type ?u.588012
M₂ : Type ?u.588015
Mₗ₁ : Type ?u.588018
Mₗ₁' : Type ?u.588021
Mₗ₂ : Type ?u.588024
Mₗ₂' : Type ?u.588027
K : Type ?u.588030
K₁ : Type ?u.588033
K₂ : Type ?u.588036
V : Type ?u.588039
V₁ : Type ?u.588042
V₂ : Type ?u.588045
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] R
v : Basis n R M
h : IsOrthoᵢ B ↑v
hB : SeparatingLeft B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
j : n
⊢ ↑(↑B (↑v i)) (↑vi j • ↑v j) = 0
case intro.h
R : Type u_1
R₁ : Type ?u.588000
R₂ : Type ?u.588003
R₃ : Type ?u.588006
M : Type u_2
M₁ : Type ?u.588012
M₂ : Type ?u.588015
Mₗ₁ : Type ?u.588018
Mₗ₁' : Type ?u.588021
Mₗ₂ : Type ?u.588024
Mₗ₂' : Type ?u.588027
K : Type ?u.588030
K₁ : Type ?u.588033
K₂ : Type ?u.588036
V : Type ?u.588039
V₁ : Type ?u.588042
V₂ : Type ?u.588045
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] R
v : Basis n R M
h : IsOrthoᵢ B ↑v
hB : SeparatingLeft B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
⊢ ∀ (x : n), x ∈ vi.support → ↑(↑B (↑v i)) (↑vi x • ↑v x) = 0
rintro j -
case intro.h
R : Type u_1
R₁ : Type ?u.588000
R₂ : Type ?u.588003
R₃ : Type ?u.588006
M : Type u_2
M₁ : Type ?u.588012
M₂ : Type ?u.588015
Mₗ₁ : Type ?u.588018
Mₗ₁' : Type ?u.588021
Mₗ₂ : Type ?u.588024
Mₗ₂' : Type ?u.588027
K : Type ?u.588030
K₁ : Type ?u.588033
K₂ : Type ?u.588036
V : Type ?u.588039
V₁ : Type ?u.588042
V₂ : Type ?u.588045
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] R
v : Basis n R M
h : IsOrthoᵢ B ↑v
hB : SeparatingLeft B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
j : n
⊢ ↑I' (↑vi j) • ↑(↑B (↑v i)) (↑v j) = 0
case intro.h
R : Type u_1
R₁ : Type ?u.588000
R₂ : Type ?u.588003
R₃ : Type ?u.588006
M : Type u_2
M₁ : Type ?u.588012
M₂ : Type ?u.588015
Mₗ₁ : Type ?u.588018
Mₗ₁' : Type ?u.588021
Mₗ₂ : Type ?u.588024
Mₗ₂' : Type ?u.588027
K : Type ?u.588030
K₁ : Type ?u.588033
K₂ : Type ?u.588036
V : Type ?u.588039
V₁ : Type ?u.588042
V₂ : Type ?u.588045
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] R
v : Basis n R M
h : IsOrthoᵢ B ↑v
hB : SeparatingLeft B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
j : n
⊢ ↑(↑B (↑v i)) (↑vi j • ↑v j) = 0
rw [map_smulₛₗ]
case intro.h
R : Type u_1
R₁ : Type ?u.588000
R₂ : Type ?u.588003
R₃ : Type ?u.588006
M : Type u_2
M₁ : Type ?u.588012
M₂ : Type ?u.588015
Mₗ₁ : Type ?u.588018
Mₗ₁' : Type ?u.588021
Mₗ₂ : Type ?u.588024
Mₗ₂' : Type ?u.588027
K : Type ?u.588030
K₁ : Type ?u.588033
K₂ : Type ?u.588036
V : Type ?u.588039
V₁ : Type ?u.588042
V₂ : Type ?u.588045
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] R
v : Basis n R M
h : IsOrthoᵢ B ↑v
hB : SeparatingLeft B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
j : n
this : ↑(↑B (↑v i)) (↑v j) = 0
⊢ ↑I' (↑vi j) • ↑(↑B (↑v i)) (↑v j) = 0

case this
R : Type u_1
R₁ : Type ?u.588000
R₂ : Type ?u.588003
R₃ : Type ?u.588006
M : Type u_2
M₁ : Type ?u.588012
M₂ : Type ?u.588015
Mₗ₁ : Type ?u.588018
Mₗ₁' : Type ?u.588021
Mₗ₂ : Type ?u.588024
Mₗ₂' : Type ?u.588027
K : Type ?u.588030
K₁ : Type ?u.588033
K₂ : Type ?u.588036
V : Type ?u.588039
V₁ : Type ?u.588042
V₂ : Type ?u.588045
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] R
v : Basis n R M
h : IsOrthoᵢ B ↑v
hB : SeparatingLeft B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
j : n
⊢ ↑(↑B (↑v i)) (↑v j) = 0
case intro.h
R : Type u_1
R₁ : Type ?u.588000
R₂ : Type ?u.588003
R₃ : Type ?u.588006
M : Type u_2
M₁ : Type ?u.588012
M₂ : Type ?u.588015
Mₗ₁ : Type ?u.588018
Mₗ₁' : Type ?u.588021
Mₗ₂ : Type ?u.588024
Mₗ₂' : Type ?u.588027
K : Type ?u.588030
K₁ : Type ?u.588033
K₂ : Type ?u.588036
V : Type ?u.588039
V₁ : Type ?u.588042
V₂ : Type ?u.588045
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] R
v : Basis n R M
h : IsOrthoᵢ B ↑v
hB : SeparatingLeft B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
j : n
⊢ ↑I' (↑vi j) • ↑(↑B (↑v i)) (↑v j) = 0
suffices : B (v i) (v j) = 0
case this.inl
R : Type u_1
R₁ : Type ?u.588000
R₂ : Type ?u.588003
R₃ : Type ?u.588006
M : Type u_2
M₁ : Type ?u.588012
M₂ : Type ?u.588015
Mₗ₁ : Type ?u.588018
Mₗ₁' : Type ?u.588021
Mₗ₂ : Type ?u.588024
Mₗ₂' : Type ?u.588027
K : Type ?u.588030
K₁ : Type ?u.588033
K₂ : Type ?u.588036
V : Type ?u.588039
V₁ : Type ?u.588042
V₂ : Type ?u.588045
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] R
v : Basis n R M
h : IsOrthoᵢ B ↑v
hB : SeparatingLeft B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
⊢ ↑(↑B (↑v i)) (↑v i) = 0

case this.inr
R : Type u_1
R₁ : Type ?u.588000
R₂ : Type ?u.588003
R₃ : Type ?u.588006
M : Type u_2
M₁ : Type ?u.588012
M₂ : Type ?u.588015
Mₗ₁ : Type ?u.588018
Mₗ₁' : Type ?u.588021
Mₗ₂ : Type ?u.588024
Mₗ₂' : Type ?u.588027
K : Type ?u.588030
K₁ : Type ?u.588033
K₂ : Type ?u.588036
V : Type ?u.588039
V₁ : Type ?u.588042
V₂ : Type ?u.588045
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] R
v : Basis n R M
h : IsOrthoᵢ B ↑v
hB : SeparatingLeft B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
j : n
hij : i ≠ j
⊢ ↑(↑B (↑v i)) (↑v j) = 0
case this
R : Type u_1
R₁ : Type ?u.588000
R₂ : Type ?u.588003
R₃ : Type ?u.588006
M : Type u_2
M₁ : Type ?u.588012
M₂ : Type ?u.588015
Mₗ₁ : Type ?u.588018
Mₗ₁' : Type ?u.588021
Mₗ₂ : Type ?u.588024
Mₗ₂' : Type ?u.588027
K : Type ?u.588030
K₁ : Type ?u.588033
K₂ : Type ?u.588036
V : Type ?u.588039
V₁ : Type ?u.588042
V₂ : Type ?u.588045
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] R
v : Basis n R M
h : IsOrthoᵢ B ↑v
hB : SeparatingLeft B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
j : n
⊢ ↑(↑B (↑v i)) (↑v j) = 0
obtain rfl | hij := eq_or_ne i j
no goals
case intro.h
R : Type u_1
R₁ : Type ?u.588000
R₂ : Type ?u.588003
R₃ : Type ?u.588006
M : Type u_2
M₁ : Type ?u.588012
M₂ : Type ?u.588015
Mₗ₁ : Type ?u.588018
Mₗ₁' : Type ?u.588021
Mₗ₂ : Type ?u.588024
Mₗ₂' : Type ?u.588027
K : Type ?u.588030
K₁ : Type ?u.588033
K₂ : Type ?u.588036
V : Type ?u.588039
V₁ : Type ?u.588042
V₂ : Type ?u.588045
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] R
v : Basis n R M
h : IsOrthoᵢ B ↑v
hB : SeparatingLeft B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
j : n
this : ↑(↑B (↑v i)) (↑v j) = 0
⊢ ↑I' (↑vi j) • ↑(↑B (↑v i)) (↑v j) = 0
rw [this, smul_eq_mul, mul_zero]
no goals
case this.inl
R : Type u_1
R₁ : Type ?u.588000
R₂ : Type ?u.588003
R₃ : Type ?u.588006
M : Type u_2
M₁ : Type ?u.588012
M₂ : Type ?u.588015
Mₗ₁ : Type ?u.588018
Mₗ₁' : Type ?u.588021
Mₗ₂ : Type ?u.588024
Mₗ₂' : Type ?u.588027
K : Type ?u.588030
K₁ : Type ?u.588033
K₂ : Type ?u.588036
V : Type ?u.588039
V₁ : Type ?u.588042
V₂ : Type ?u.588045
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] R
v : Basis n R M
h : IsOrthoᵢ B ↑v
hB : SeparatingLeft B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
⊢ ↑(↑B (↑v i)) (↑v i) = 0
exact ho
no goals
case this.inr
R : Type u_1
R₁ : Type ?u.588000
R₂ : Type ?u.588003
R₃ : Type ?u.588006
M : Type u_2
M₁ : Type ?u.588012
M₂ : Type ?u.588015
Mₗ₁ : Type ?u.588018
Mₗ₁' : Type ?u.588021
Mₗ₂ : Type ?u.588024
Mₗ₂' : Type ?u.588027
K : Type ?u.588030
K₁ : Type ?u.588033
K₂ : Type ?u.588036
V : Type ?u.588039
V₁ : Type ?u.588042
V₂ : Type ?u.588045
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : Nontrivial R
B : M →ₛₗ[I] M →ₛₗ[I'] R
v : Basis n R M
h : IsOrthoᵢ B ↑v
hB : SeparatingLeft B
i : n
ho : IsOrtho B (↑v i) (↑v i)
vi : n →₀ R
j : n
hij : i ≠ j
⊢ ↑(↑B (↑v i)) (↑v j) = 0
exact h hij