C_eq_natCast

Mathlib.Algebra.Polynomial.Basic

URI: https://scilib.ai/kg/mathlib#Polynomial.C_eq_natCast

English

For every natural number n, C(n) equals the natural cast of n as a polynomial: C(n) = (n : R[X]).

Русский

Для каждого натурального числа n выполняется C(n) = (n : R[X]).

LaTeX

$$$ C(n) = (n : R[X]) $$$

Lean4

theorem C_eq_natCast (n : ℕ) : C (n : R) = (n : R[X]) :=
  map_natCast C n

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

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

Разделы

Аффилиация

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