irreducible_of_isCoprime — Mathlib

English

A unit trinomial p is irreducible if it is coprime with its mirror; this is stated as Irreducible p given hp IsUnitTrinomial and h IsCoprime p p.mirror.

Русский

Единичный триномиал p неразложим, если он взаимно прост с зеркальным p; то есть Irreducible p при hp IsUnitTrinomial и h IsCoprime p p.mirror.

LaTeX

$$IsUnitTrinomial(p) ∧ IsCoprime(p, p.mirror) ⇒ Irreducible(p)$$

Lean4

/-- A unit trinomial is irreducible if it is coprime with its mirror -/
theorem irreducible_of_isCoprime (hp : p.IsUnitTrinomial) (h : IsCoprime p p.mirror) : Irreducible p :=
  irreducible_of_coprime hp fun _ => h.isUnit_of_dvd'

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