coe — Mathlib

English

There is a canonical map from real numbers to angles, sending r to its class modulo 2πZ.

Русский

Существует каноническое отображение из ℝ в угол, отправляющее r в его класс по модулю 2πZ.

LaTeX

$$$$ \text{coe}: \mathbb{R} \to \text{Angle},\quad \text{coe}(r) = [r] \in \mathbb{R}/(2\pi\mathbb{Z}). $$$$

Lean4

/-- The canonical map from `ℝ` to the quotient `Angle`. -/
@[coe]
protected def coe (r : ℝ) : Angle :=
  QuotientAddGroup.mk r

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