case mp
R : Type u_2
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
h : mulLeft R a = 0
⊢ a = 0

case mpr
R : Type u_2
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
h : a = 0
⊢ mulLeft R a = 0
R : Type u_2
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ mulLeft R a = 0 ↔ a = 0
constructor <;> intro h
no goals
case mp
R : Type u_2
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
h : mulLeft R a = 0
⊢ a = 0
rw [← mul_one a, ← @mulLeft_apply R _ _ _ _ _ _ a 1, h, LinearMap.zero_apply]
case mpr
R : Type u_2
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
h : a = 0
⊢ mulLeft R 0 = 0
case mpr
R : Type u_2
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
h : a = 0
⊢ mulLeft R a = 0
rw [h]
no goals
case mpr
R : Type u_2
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
h : a = 0
⊢ mulLeft R 0 = 0
exact mulLeft_zero_eq_zero