case inl
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
a : A
ha : Set.Nonempty (σ a)
⊢ σ (0 • a) = 0 • σ a

case inr
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
k : 𝕜
a : A
ha : Set.Nonempty (σ a)
h : k ≠ 0
⊢ σ (k • a) = k • σ a
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
k : 𝕜
a : A
ha : Set.Nonempty (σ a)
⊢ σ (k • a) = k • σ a
rcases eq_or_ne k 0 with (rfl | h)
no goals
case inl
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
a : A
ha : Set.Nonempty (σ a)
⊢ σ (0 • a) = 0 • σ a
simpa [ha, zero_smul_set] using (show {(0 : 𝕜)} = (0 : Set 𝕜) from rfl)
no goals
case inr
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
k : 𝕜
a : A
ha : Set.Nonempty (σ a)
h : k ≠ 0
⊢ σ (k • a) = k • σ a
exact unit_smul_eq_smul a (Units.mk0 k h)