toUnits_apply — Mathlib

English

The action of toUnits on an element z of Circle is the expected Units element given by the underlying complex coordinate.

Русский

Действие toUnits на элементе z круга даёт единичный элемент, соответствующий его базовой комплексной координате.

LaTeX

$$$$ toUnits(z) = \\mathrm{Units.mk0}(\\uparrow z) \\; z_{\\mathrm{coe\\_ne\\_zero}}. $$$$

Lean4

@[simp]
theorem toUnits_apply (z : Circle) : toUnits z = Units.mk0 (↑z) z.coe_ne_zero :=
  rfl

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