smul_add — Mathlib

English

smul distributes over addition: z • (x + y) = z • x + z • y.

Русский

распределение скаляра над сложением: z • (x + y) = z • x + z • y.

LaTeX

$$$z \cdot (x + y) = z \cdot x + z \cdot y$$$

Lean4

protected theorem smul_add (z : R[S⁻¹]) (x y : X[S⁻¹]) : z • (x + y) = z • x + z • y :=
  by
  induction x with
  | _ r₁ s₁
  induction y with
  | _ r₂ s₂
  induction z with
  | _ r₃ s₃
  rcases oreDivAddChar' r₁ r₂ s₁ s₂ with ⟨ra, sa, ha, ha'⟩; rw [ha']; clear ha'; norm_cast at ha
  rw [OreLocalization.expand' r₁ s₁ sa]
  rw [OreLocalization.expand r₂ s₂ ra (by rw [← ha]; apply SetLike.coe_mem)]
  rw [← Subtype.coe_eq_of_eq_mk ha]
  repeat rw [oreDiv_smul_oreDiv]
  simp only [smul_add, add_oreDiv]

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