ofInt_eq_cast — Mathlib

English

For each integer n, the embedding of integers into rationals via ofInt equals the standard integer cast into rationals: ofInt n = Int.cast n.

Русский

Для целого n вложение целых чисел в рациональные через ofInt совпадает с обычным приведением: ofInt n = Int.cast n.

LaTeX

$$$\operatorname{ofInt}(n) = \operatorname{Int.cast}(n)$$$

Lean4

@[simp]
theorem ofInt_eq_cast (n : ℤ) : ofInt n = Int.cast n :=
  rfl

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