ofDual_ratCast — Mathlib

English

Let K be a type equipped with a canonical embedding of rationals into K. Then for every rational n, the image of n in K under this embedding equals n viewed as an element of K.

Русский

Пусть K имеет каноническое отображение чисел ℚ в K. Тогда для любого рационального числа n образ n в K по этому отображению равен n как элементу K.

LaTeX

$$$\forall n \in \mathbb{Q}, \\iota(n) = n$$$

Lean4

@[simp]
theorem ofDual_ratCast [RatCast K] (n : ℚ) : (ofDual n : K) = n :=
  rfl

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