ofRat_intCast

Mathlib.Algebra.Order.CauSeq.Completion

URI: https://scilib.ai/kg/mathlib#CauSeq.Completion.ofRat_intCast

English

ofRat z = z for z ∈ ℤ, i.e. integers embed identically.

Русский

ofRat z = z для z ∈ ℤ, то есть целые числа встраиваются идентично.

LaTeX

$$$\operatorname{ofRat}(z) = z$$$

Lean4

@[simp]
theorem ofRat_intCast (z : ℤ) : (ofRat z : Cauchy abv) = z :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru