R : Type u_1
R₁ : Type ?u.576918
R₂ : Type ?u.576921
R₃ : Type ?u.576924
M : Type u_2
M₁ : Type ?u.576930
M₂ : Type ?u.576933
Mₗ₁ : Type ?u.576936
Mₗ₁' : Type ?u.576939
Mₗ₂ : Type ?u.576942
Mₗ₂' : Type ?u.576945
K : Type ?u.576948
K₁ : Type ?u.576951
K₂ : Type ?u.576954
V : Type ?u.576957
V₁ : Type ?u.576960
V₂ : Type ?u.576963
n : Type ?u.576966
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
hB' : SeparatingRight B
⊢ SeparatingLeft B
R : Type u_1
R₁ : Type ?u.576918
R₂ : Type ?u.576921
R₃ : Type ?u.576924
M : Type u_2
M₁ : Type ?u.576930
M₂ : Type ?u.576933
Mₗ₁ : Type ?u.576936
Mₗ₁' : Type ?u.576939
Mₗ₂ : Type ?u.576942
Mₗ₂' : Type ?u.576945
K : Type ?u.576948
K₁ : Type ?u.576951
K₂ : Type ?u.576954
V : Type ?u.576957
V₁ : Type ?u.576960
V₂ : Type ?u.576963
n : Type ?u.576966
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
hB' : SeparatingRight B
⊢ Nondegenerate B
refine' ⟨_, hB'⟩
R : Type u_1
R₁ : Type ?u.576918
R₂ : Type ?u.576921
R₃ : Type ?u.576924
M : Type u_2
M₁ : Type ?u.576930
M₂ : Type ?u.576933
Mₗ₁ : Type ?u.576936
Mₗ₁' : Type ?u.576939
Mₗ₂ : Type ?u.576942
Mₗ₂' : Type ?u.576945
K : Type ?u.576948
K₁ : Type ?u.576951
K₂ : Type ?u.576954
V : Type ?u.576957
V₁ : Type ?u.576960
V₂ : Type ?u.576963
n : Type ?u.576966
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
hB' : SeparatingRight B
⊢ ker (flip B) = ⊥
R : Type u_1
R₁ : Type ?u.576918
R₂ : Type ?u.576921
R₃ : Type ?u.576924
M : Type u_2
M₁ : Type ?u.576930
M₂ : Type ?u.576933
Mₗ₁ : Type ?u.576936
Mₗ₁' : Type ?u.576939
Mₗ₂ : Type ?u.576942
Mₗ₂' : Type ?u.576945
K : Type ?u.576948
K₁ : Type ?u.576951
K₂ : Type ?u.576954
V : Type ?u.576957
V₁ : Type ?u.576960
V₂ : Type ?u.576963
n : Type ?u.576966
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
hB' : SeparatingRight B
⊢ SeparatingLeft B
rw [separatingLeft_iff_ker_eq_bot, hB.ker_eq_bot_iff_ker_flip_eq_bot.mpr]
no goals
R : Type u_1
R₁ : Type ?u.576918
R₂ : Type ?u.576921
R₃ : Type ?u.576924
M : Type u_2
M₁ : Type ?u.576930
M₂ : Type ?u.576933
Mₗ₁ : Type ?u.576936
Mₗ₁' : Type ?u.576939
Mₗ₂ : Type ?u.576942
Mₗ₂' : Type ?u.576945
K : Type ?u.576948
K₁ : Type ?u.576951
K₂ : Type ?u.576954
V : Type ?u.576957
V₁ : Type ?u.576960
V₂ : Type ?u.576963
n : Type ?u.576966
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
hB' : SeparatingRight B
⊢ ker (flip B) = ⊥
rwa [← separatingRight_iff_flip_ker_eq_bot]