polynomial_not_isField — Mathlib

English

For any ring R, the polynomial ring R[X] is not a field.

Русский

Для любого кольца R кольцо полиномов R[X] не является полем.

LaTeX

$$$\\forall R\\ (\\text{IsRing } R) \\Rightarrow \\neg IsField(R[X])$$$

Lean4

/-- `R[X]` is never a field for any ring `R`. -/
theorem polynomial_not_isField : ¬IsField R[X] := by
  nontriviality R
  intro hR
  obtain ⟨p, hp⟩ := hR.mul_inv_cancel X_ne_zero
  have hp0 : p ≠ 0 := right_ne_zero_of_mul_eq_one hp
  have := degree_lt_degree_mul_X hp0
  rw [← X_mul, congr_arg degree hp, degree_one, Nat.WithBot.lt_zero_iff, degree_eq_bot] at this
  exact hp0 this

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