smul_eq_smul — Mathlib

English

If (σ(a)).Nonempty, then σ(k a) = k · σ(a) for k ∈ 𝕜 and a ∈ A, provided A is nontrivial.

Русский

Если (σ(a)) непусто, то σ(k a) = k · σ(a) для k ∈ 𝕜 и a ∈ A при условии ненулевой алгебры.

LaTeX

$$$\text{If } (\sigma_R(a)).\text{Nonempty}, \quad σ_R(k \cdot a) = k \cdot σ_R(a)$$$

Lean4

/-- the assumption `(σ a).Nonempty` is necessary and cannot be removed without
further conditions on the algebra `A` and scalar field `𝕜`. -/
theorem smul_eq_smul [Nontrivial A] (k : 𝕜) (a : A) (ha : (σ a).Nonempty) : σ (k • a) = k • σ a :=
  by
  rcases eq_or_ne k 0 with (rfl | h)
  · simpa [ha, zero_smul_set] using (show {(0 : 𝕜)} = (0 : Set 𝕜) from rfl)
  · exact unit_smul_eq_smul a (Units.mk0 k h)

Похожие утверждения