int_leadingCoeff_eq

Mathlib.Algebra.Ring.Subring.IntPolynomial

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

English

The leading coefficient of P.int R hP, viewed in K, equals the leading coefficient of P.

Русский

Передний коэффициент P.int R hP, приведённый к K, равен ведущему коэффициенту P.

LaTeX

$$$\uparrow\!(P.int R hP).leadingCoeff = P.leadingCoeff$$$

Lean4

@[simp]
theorem int_leadingCoeff_eq : ↑(P.int R hP).leadingCoeff = P.leadingCoeff :=
  rfl

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

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

Разделы

Аффилиация

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