R : Type u_1
R₁ : Type u_2
R₂ : Type ?u.124036
R₃ : Type ?u.124039
M : Type ?u.124042
M₁ : Type u_3
M₂ : Type ?u.124048
Mₗ₁ : Type ?u.124051
Mₗ₁' : Type ?u.124054
Mₗ₂ : Type ?u.124057
Mₗ₂' : Type ?u.124060
K : Type ?u.124063
K₁ : Type ?u.124066
K₂ : Type ?u.124069
V : Type ?u.124072
V₁ : Type ?u.124075
V₂ : Type ?u.124078
n : Type ?u.124081
inst✝³ : CommSemiring R
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
H✝ H : IsRefl B
h : ker (flip B) = ⊥
⊢ ker B = ⊥
R : Type u_1
R₁ : Type u_2
R₂ : Type ?u.124036
R₃ : Type ?u.124039
M : Type ?u.124042
M₁ : Type u_3
M₂ : Type ?u.124048
Mₗ₁ : Type ?u.124051
Mₗ₁' : Type ?u.124054
Mₗ₂ : Type ?u.124057
Mₗ₂' : Type ?u.124060
K : Type ?u.124063
K₁ : Type ?u.124066
K₂ : Type ?u.124069
V : Type ?u.124072
V₁ : Type ?u.124075
V₂ : Type ?u.124078
n : Type ?u.124081
inst✝³ : CommSemiring R
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
H✝ H : IsRefl B
⊢ ker B = ⊥ ↔ ker (flip B) = ⊥
refine' ⟨ker_flip_eq_bot H, fun h ↦ _⟩
no goals
R : Type u_1
R₁ : Type u_2
R₂ : Type ?u.124036
R₃ : Type ?u.124039
M : Type ?u.124042
M₁ : Type u_3
M₂ : Type ?u.124048
Mₗ₁ : Type ?u.124051
Mₗ₁' : Type ?u.124054
Mₗ₂ : Type ?u.124057
Mₗ₂' : Type ?u.124060
K : Type ?u.124063
K₁ : Type ?u.124066
K₂ : Type ?u.124069
V : Type ?u.124072
V₁ : Type ?u.124075
V₂ : Type ?u.124078
n : Type ?u.124081
inst✝³ : CommSemiring R
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R
H✝ H : IsRefl B
h : ker (flip B) = ⊥
⊢ ker B = ⊥
exact (congr_arg _ B.flip_flip.symm).trans (ker_flip_eq_bot (flip_isRefl_iff.mpr H) h)