R : Type u_1
R₁ : Type ?u.611950
R₂ : Type ?u.611953
R₃ : Type ?u.611956
M : Type u_2
M₁ : Type ?u.611962
M₂ : Type ?u.611965
Mₗ₁ : Type ?u.611968
Mₗ₁' : Type ?u.611971
Mₗ₂ : Type ?u.611974
Mₗ₂' : Type ?u.611977
K : Type ?u.611980
K₁ : Type ?u.611983
K₂ : Type ?u.611986
V : Type ?u.611989
V₁ : Type ?u.611992
V₂ : Type ?u.611995
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ (flip B) ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
⊢ SeparatingRight B
R : Type u_1
R₁ : Type ?u.611950
R₂ : Type ?u.611953
R₃ : Type ?u.611956
M : Type u_2
M₁ : Type ?u.611962
M₂ : Type ?u.611965
Mₗ₁ : Type ?u.611968
Mₗ₁' : Type ?u.611971
Mₗ₂ : Type ?u.611974
Mₗ₂' : Type ?u.611977
K : Type ?u.611980
K₁ : Type ?u.611983
K₂ : Type ?u.611986
V : Type ?u.611989
V₁ : Type ?u.611992
V₂ : Type ?u.611995
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ B ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
⊢ SeparatingRight B
rw [isOrthoᵢ_flip] at hO
R : Type u_1
R₁ : Type ?u.611950
R₂ : Type ?u.611953
R₃ : Type ?u.611956
M : Type u_2
M₁ : Type ?u.611962
M₂ : Type ?u.611965
Mₗ₁ : Type ?u.611968
Mₗ₁' : Type ?u.611971
Mₗ₂ : Type ?u.611974
Mₗ₂' : Type ?u.611977
K : Type ?u.611980
K₁ : Type ?u.611983
K₂ : Type ?u.611986
V : Type ?u.611989
V₁ : Type ?u.611992
V₂ : Type ?u.611995
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ (flip B) ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
⊢ SeparatingLeft (flip B)
R : Type u_1
R₁ : Type ?u.611950
R₂ : Type ?u.611953
R₃ : Type ?u.611956
M : Type u_2
M₁ : Type ?u.611962
M₂ : Type ?u.611965
Mₗ₁ : Type ?u.611968
Mₗ₁' : Type ?u.611971
Mₗ₂ : Type ?u.611974
Mₗ₂' : Type ?u.611977
K : Type ?u.611980
K₁ : Type ?u.611983
K₂ : Type ?u.611986
V : Type ?u.611989
V₁ : Type ?u.611992
V₂ : Type ?u.611995
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ (flip B) ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
⊢ SeparatingRight B
rw [← flip_separatingLeft]
R : Type u_1
R₁ : Type ?u.611950
R₂ : Type ?u.611953
R₃ : Type ?u.611956
M : Type u_2
M₁ : Type ?u.611962
M₂ : Type ?u.611965
Mₗ₁ : Type ?u.611968
Mₗ₁' : Type ?u.611971
Mₗ₂ : Type ?u.611974
Mₗ₂' : Type ?u.611977
K : Type ?u.611980
K₁ : Type ?u.611983
K₂ : Type ?u.611986
V : Type ?u.611989
V₁ : Type ?u.611992
V₂ : Type ?u.611995
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ (flip B) ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
i : n
⊢ ¬IsOrtho (flip B) (↑v i) (↑v i)
R : Type u_1
R₁ : Type ?u.611950
R₂ : Type ?u.611953
R₃ : Type ?u.611956
M : Type u_2
M₁ : Type ?u.611962
M₂ : Type ?u.611965
Mₗ₁ : Type ?u.611968
Mₗ₁' : Type ?u.611971
Mₗ₂ : Type ?u.611974
Mₗ₂' : Type ?u.611977
K : Type ?u.611980
K₁ : Type ?u.611983
K₂ : Type ?u.611986
V : Type ?u.611989
V₁ : Type ?u.611992
V₂ : Type ?u.611995
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ (flip B) ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
⊢ SeparatingLeft (flip B)
refine' IsOrthoᵢ.separatingLeft_of_not_isOrtho_basis_self v hO fun i ↦ _
R : Type u_1
R₁ : Type ?u.611950
R₂ : Type ?u.611953
R₃ : Type ?u.611956
M : Type u_2
M₁ : Type ?u.611962
M₂ : Type ?u.611965
Mₗ₁ : Type ?u.611968
Mₗ₁' : Type ?u.611971
Mₗ₂ : Type ?u.611974
Mₗ₂' : Type ?u.611977
K : Type ?u.611980
K₁ : Type ?u.611983
K₂ : Type ?u.611986
V : Type ?u.611989
V₁ : Type ?u.611992
V₂ : Type ?u.611995
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ (flip B) ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
i : n
⊢ ¬IsOrtho (flip (flip B)) (↑v i) (↑v i)
R : Type u_1
R₁ : Type ?u.611950
R₂ : Type ?u.611953
R₃ : Type ?u.611956
M : Type u_2
M₁ : Type ?u.611962
M₂ : Type ?u.611965
Mₗ₁ : Type ?u.611968
Mₗ₁' : Type ?u.611971
Mₗ₂ : Type ?u.611974
Mₗ₂' : Type ?u.611977
K : Type ?u.611980
K₁ : Type ?u.611983
K₂ : Type ?u.611986
V : Type ?u.611989
V₁ : Type ?u.611992
V₂ : Type ?u.611995
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ (flip B) ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
i : n
⊢ ¬IsOrtho (flip B) (↑v i) (↑v i)
rw [isOrtho_flip]
no goals
R : Type u_1
R₁ : Type ?u.611950
R₂ : Type ?u.611953
R₃ : Type ?u.611956
M : Type u_2
M₁ : Type ?u.611962
M₂ : Type ?u.611965
Mₗ₁ : Type ?u.611968
Mₗ₁' : Type ?u.611971
Mₗ₂ : Type ?u.611974
Mₗ₂' : Type ?u.611977
K : Type ?u.611980
K₁ : Type ?u.611983
K₂ : Type ?u.611986
V : Type ?u.611989
V₁ : Type ?u.611992
V₂ : Type ?u.611995
n : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I I' : R →+* R
inst✝ : NoZeroDivisors R
B : M →ₗ[R] M →ₗ[R] R
v : Basis n R M
hO : IsOrthoᵢ (flip B) ↑v
h : ∀ (i : n), ¬IsOrtho B (↑v i) (↑v i)
i : n
⊢ ¬IsOrtho (flip (flip B)) (↑v i) (↑v i)
exact h i