snd_mul — Mathlib

English

The second component of the product in a dual-number algebra is given by the rule: snd(x·y) = fst(x)·snd(y) + snd(x)·fst(y).

Русский

В системе двойных чисел второй координатой произведения является snd(x·y) = fst(x)·snd(y) + snd(x)·fst(y).

LaTeX

$$$\mathrm{snd}(x \cdot y) = \mathrm{fst}(x) \cdot \mathrm{snd}(y) + \mathrm{snd}(x) \cdot \mathrm{fst}(y)$$$

Lean4

/-- A version of `TrivSqZeroExt.snd_mul` with `*` instead of `•`. -/
@[simp]
theorem snd_mul [Semiring R] (x y : R[ε]) : snd (x * y) = fst x * snd y + snd x * fst y :=
  rfl

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