R : Type u_1
R₁ : Type ?u.572349
R₂ : Type ?u.572352
R₃ : Type ?u.572355
M : Type u_2
M₁ : Type ?u.572361
M₂ : Type ?u.572364
Mₗ₁ : Type ?u.572367
Mₗ₁' : Type ?u.572370
Mₗ₂ : Type ?u.572373
Mₗ₂' : Type ?u.572376
K : Type ?u.572379
K₁ : Type ?u.572382
K₂ : Type ?u.572385
V : Type ?u.572388
V₁ : Type ?u.572391
V₂ : Type ?u.572394
n : Type ?u.572397
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
hB' : SeparatingLeft B
⊢ SeparatingRight B
R : Type u_1
R₁ : Type ?u.572349
R₂ : Type ?u.572352
R₃ : Type ?u.572355
M : Type u_2
M₁ : Type ?u.572361
M₂ : Type ?u.572364
Mₗ₁ : Type ?u.572367
Mₗ₁' : Type ?u.572370
Mₗ₂ : Type ?u.572373
Mₗ₂' : Type ?u.572376
K : Type ?u.572379
K₁ : Type ?u.572382
K₂ : Type ?u.572385
V : Type ?u.572388
V₁ : Type ?u.572391
V₂ : Type ?u.572394
n : Type ?u.572397
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
hB' : SeparatingLeft B
⊢ Nondegenerate B
refine' ⟨hB', _⟩
R : Type u_1
R₁ : Type ?u.572349
R₂ : Type ?u.572352
R₃ : Type ?u.572355
M : Type u_2
M₁ : Type ?u.572361
M₂ : Type ?u.572364
Mₗ₁ : Type ?u.572367
Mₗ₁' : Type ?u.572370
Mₗ₂ : Type ?u.572373
Mₗ₂' : Type ?u.572376
K : Type ?u.572379
K₁ : Type ?u.572382
K₂ : Type ?u.572385
V : Type ?u.572388
V₁ : Type ?u.572391
V₂ : Type ?u.572394
n : Type ?u.572397
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
hB' : SeparatingLeft B
⊢ ker B = ⊥
R : Type u_1
R₁ : Type ?u.572349
R₂ : Type ?u.572352
R₃ : Type ?u.572355
M : Type u_2
M₁ : Type ?u.572361
M₂ : Type ?u.572364
Mₗ₁ : Type ?u.572367
Mₗ₁' : Type ?u.572370
Mₗ₂ : Type ?u.572373
Mₗ₂' : Type ?u.572376
K : Type ?u.572379
K₁ : Type ?u.572382
K₂ : Type ?u.572385
V : Type ?u.572388
V₁ : Type ?u.572391
V₂ : Type ?u.572394
n : Type ?u.572397
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
hB' : SeparatingLeft B
⊢ SeparatingRight B
rw [separatingRight_iff_flip_ker_eq_bot, hB.ker_eq_bot_iff_ker_flip_eq_bot.mp]
no goals
R : Type u_1
R₁ : Type ?u.572349
R₂ : Type ?u.572352
R₃ : Type ?u.572355
M : Type u_2
M₁ : Type ?u.572361
M₂ : Type ?u.572364
Mₗ₁ : Type ?u.572367
Mₗ₁' : Type ?u.572370
Mₗ₂ : Type ?u.572373
Mₗ₂' : Type ?u.572376
K : Type ?u.572379
K₁ : Type ?u.572382
K₂ : Type ?u.572385
V : Type ?u.572388
V₁ : Type ?u.572391
V₂ : Type ?u.572394
n : Type ?u.572397
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I I' : R →+* R
B : M →ₗ[R] M →ₗ[R] R
hB : IsRefl B
hB' : SeparatingLeft B
⊢ ker B = ⊥
rwa [← separatingLeft_iff_ker_eq_bot]