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