star_eq_two_re_sub — Mathlib

English

The star of a equals the subtraction of a from the embedding of twice the real part plus c2 times the imaginary part: star a = ↑(2 a.re + c2 a.imI) − a.

Русский

Звезда элемента a равна вычитанию самого a из встраивания двойного вещественного центра плюс c2 раза мнимая часть: star a = ↑(2 a.re + c2 a.imI) − a.

LaTeX

$$$\text{star } a = \uparrow (2 \cdot a.re + c_2 \cdot a.imI) - a$$$

Lean4

theorem star_eq_two_re_sub : star a = ↑(2 * a.re + c₂ * a.imI) - a :=
  eq_sub_iff_add_eq.2 a.star_add_self'

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