coe_ratCast — Mathlib

English

Rational numbers embed compatibly: the algebra map sends q ∈ ℚ to q in A via the rational cast.

Русский

Рациональные числа включаются совместимо: карта алгебры отправляет q ∈ ℚ в q в A через приведение рационального числа.

LaTeX

$$$ ↑(q : \\mathbb{Q}) = (q : A) \\quad (q \\in \\mathbb{Q}).$$$

Lean4

@[norm_cast]
theorem coe_ratCast (q : ℚ) : ↑(q : R) = (q : A) :=
  map_ratCast (algebraMap R A) q

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