rotation_apply — Mathlib

English

The rotation by a unit circle element a acts on any complex z by ordinary multiplication: rotation a (z) = a z.

Русский

Поворот элементом единичной окружности действует на комплексное число z обычным умножением: rotation a (z) = a z.

LaTeX

$$$\forall a \in \mathbb{C}_{1}, \forall z \in \mathbb{C},\;\text{rotation}(a)(z) = a z$$$

Lean4

@[simp]
theorem rotation_apply (a : Circle) (z : ℂ) : rotation a z = a * z :=
  rfl

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