monic_denom

Mathlib.FieldTheory.RatFunc.Basic

URI: https://scilib.ai/kg/mathlib#RatFunc.monic_denom

← MathLib Explorer

English

The denominator is monic: Monic(denom(x)).

Русский

Знаменатель моничен: Monic(denom(x)).

LaTeX

$$$\operatorname{Monic}\left(\operatorname{denom}(x)\right)$$$

Lean4

theorem monic_denom (x : RatFunc K) : (denom x).Monic := by
  classical
    induction x using RatFunc.induction_on with
  | f p q hq =>
    rw [denom_div p hq, mul_comm]
    exact Polynomial.monic_mul_leadingCoeff_inv (right_div_gcd_ne_zero hq)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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