R : Type u_1
R₁ : Type ?u.596990
R₂ : Type ?u.596993
R₃ : Type ?u.596996
M : Type u_2
M₁ : Type ?u.597002
M₂ : Type ?u.597005
Mₗ₁ : Type ?u.597008
Mₗ₁' : Type ?u.597011
Mₗ₂ : Type ?u.597014
Mₗ₂' : Type ?u.597017
K : Type ?u.597020
K₁ : Type ?u.597023
K₂ : Type ?u.597026
V : Type ?u.597029
V₁ : Type ?u.597032
V₂ : Type ?u.597035
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ᵢ (flip B) ↑v
hB : SeparatingRight B
i : n
⊢ ¬IsOrtho B (↑v i) (↑v i)
R : Type u_1
R₁ : Type ?u.596990
R₂ : Type ?u.596993
R₃ : Type ?u.596996
M : Type u_2
M₁ : Type ?u.597002
M₂ : Type ?u.597005
Mₗ₁ : Type ?u.597008
Mₗ₁' : Type ?u.597011
Mₗ₂ : Type ?u.597014
Mₗ₂' : Type ?u.597017
K : Type ?u.597020
K₁ : Type ?u.597023
K₂ : Type ?u.597026
V : Type ?u.597029
V₁ : Type ?u.597032
V₂ : Type ?u.597035
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 : SeparatingRight B
i : n
⊢ ¬IsOrtho B (↑v i) (↑v i)
rw [isOrthoᵢ_flip] at h
R : Type u_1
R₁ : Type ?u.596990
R₂ : Type ?u.596993
R₃ : Type ?u.596996
M : Type u_2
M₁ : Type ?u.597002
M₂ : Type ?u.597005
Mₗ₁ : Type ?u.597008
Mₗ₁' : Type ?u.597011
Mₗ₂ : Type ?u.597014
Mₗ₂' : Type ?u.597017
K : Type ?u.597020
K₁ : Type ?u.597023
K₂ : Type ?u.597026
V : Type ?u.597029
V₁ : Type ?u.597032
V₂ : Type ?u.597035
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ᵢ (flip B) ↑v
hB : SeparatingRight B
i : n
⊢ ¬IsOrtho (flip B) (↑v i) (↑v i)
R : Type u_1
R₁ : Type ?u.596990
R₂ : Type ?u.596993
R₃ : Type ?u.596996
M : Type u_2
M₁ : Type ?u.597002
M₂ : Type ?u.597005
Mₗ₁ : Type ?u.597008
Mₗ₁' : Type ?u.597011
Mₗ₂ : Type ?u.597014
Mₗ₂' : Type ?u.597017
K : Type ?u.597020
K₁ : Type ?u.597023
K₂ : Type ?u.597026
V : Type ?u.597029
V₁ : Type ?u.597032
V₂ : Type ?u.597035
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ᵢ (flip B) ↑v
hB : SeparatingRight B
i : n
⊢ ¬IsOrtho B (↑v i) (↑v i)
rw [isOrtho_flip]
no goals
R : Type u_1
R₁ : Type ?u.596990
R₂ : Type ?u.596993
R₃ : Type ?u.596996
M : Type u_2
M₁ : Type ?u.597002
M₂ : Type ?u.597005
Mₗ₁ : Type ?u.597008
Mₗ₁' : Type ?u.597011
Mₗ₂ : Type ?u.597014
Mₗ₂' : Type ?u.597017
K : Type ?u.597020
K₁ : Type ?u.597023
K₂ : Type ?u.597026
V : Type ?u.597029
V₁ : Type ?u.597032
V₂ : Type ?u.597035
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ᵢ (flip B) ↑v
hB : SeparatingRight B
i : n
⊢ ¬IsOrtho (flip B) (↑v i) (↑v i)
exact h.not_isOrtho_basis_self_of_separatingLeft (flip_separatingLeft.mpr hB) i