coe_intCast — Mathlib

English

For all integers n, the integer embedding into the quotient agrees with the integer n: (↑(n : R) : c.Quotient) = n.

Русский

Для всех целых чисел n отображение целого числа в Quotient совпадает с n: ↑(n : R) = n в Quotient.

LaTeX

$$$$\left( ↑(n : R) : c.Quotient \right) = n \quad \text{for all } n \in \mathbb{Z}.$$$$

Lean4

@[simp, norm_cast]
theorem coe_intCast (n : ℕ) : (↑(n : R) : c.Quotient) = n :=
  rfl

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