instGroupWithZero — Mathlib

English

If f is irreducible, then the structure on AdjoinRoot f given by quotient by the ideal generated by f yields a GroupWithZero, i.e., AdjoinRoot f is a field and carries a multiplicative group with zero.

Русский

Если f ирредуцируемый, то структура AdjoinRoot f, полученная как деление по идеалу (f), образует GroupWithZero, то есть является полем и имеет группу с нулём.

LaTeX

$$IsGroupWithZero(AdjoinRoot f) follows from Irreducible f$$

Lean4

noncomputable instance instGroupWithZero [Fact (Irreducible f)] : GroupWithZero (AdjoinRoot f) :=
  Quotient.groupWithZero (span { f } : Ideal K[X])

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