isAlgebraic_rat — Mathlib

English

For any rational number n, n cast into A is algebraic over R.

Русский

Для рационального числа n константа n в A алгебраична над R.

LaTeX

$$$ (R : Type u) {A : Type v} [DivisionRing A] [Field R] [Algebra R A] (n : \mathbb{Q}) : IsAlgebraic R (n.cast) $$$

Lean4

theorem isAlgebraic_rat (R : Type u) {A : Type v} [DivisionRing A] [Field R] [Algebra R A] (n : ℚ) :
    IsAlgebraic R (n : A) := by
  rw [← map_ratCast (algebraMap R A)]
  exact isAlgebraic_algebraMap (Rat.cast n)

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