not_isField — Mathlib

English

p equals (X - C a)^{rootMultiplicity a p} times the quotient p /ₘ (X - C a)^{rootMultiplicity a p}.

Русский

p равно (X − C a)^{rootMultiplicity a p} умножить на частное p /ₘ (X − C a)^{rootMultiplicity a p}.

LaTeX

$$$$ (X - C a)^{\\operatorname{rootMultiplicity} a p} \\cdot \\left(p /ₘ (X - C a)^{\\operatorname{rootMultiplicity} a p}\\right) = p. $$$$

Lean4

theorem not_isField : ¬IsField R[X] := by
  nontriviality R
  intro h
  letI := h.toField
  simpa using congr_arg natDegree (monic_X.eq_one_of_isUnit <| monic_X (R := R).ne_zero.isUnit)

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