re_add — Mathlib

English

The real part distributes over quaternion addition: the real part of a + b equals the sum of the real parts.

Русский

Действительная часть добавления кватернионов распадается на сумму действительных частей: Re(a + b) = Re(a) + Re(b).

LaTeX

$$$$\forall a,b \in \mathbb{H}(R):\ \operatorname{Re}(a + b) = \operatorname{Re}(a) + \operatorname{Re}(b).$$$$

Lean4

@[simp]
theorem re_add : (a + b).re = a.re + b.re :=
  rfl

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