toDual_ratCast — Mathlib

English

If K has a RatCast, then for every rational n, the dual embedding agrees with the scalar n, i.e., toDual(n) = n.

Русский

Если у K есть отображение рациональных чисел в K, то для каждого рационального числа n выполняется toDual(n) = n.

LaTeX

$$$\\mathrm{toDual}(n) = n \\quad( n \\in \\mathbb{Q} )$$$

Lean4

@[simp]
theorem toDual_ratCast [RatCast K] (n : ℚ) : toDual (n : K) = n :=
  rfl

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