not_isLocalRing_of_prod_of_nontrivial

English

The product of two nontrivial semirings is not local.

Русский

Произведение двух не тривиальных полей не является локальным кольцом.

LaTeX

$$$ \neg IsLocalRing (R_1 \times R_2). $$$

Lean4

/-- The product of two nontrivial (semi)rings is not local. -/
theorem not_isLocalRing_of_prod_of_nontrivial (R₁ R₂ : Type*) [Semiring R₁] [Semiring R₂] [Nontrivial R₁]
    [Nontrivial R₂] : ¬IsLocalRing (R₁ × R₂) :=
  have ha : ¬IsUnit ((1, 0) : R₁ × R₂) := fun h ↦ not_isUnit_zero (M₀ := R₁) (by simpa using h.map (RingHom.snd R₁ R₂))
  have hb : ¬IsUnit ((0, 1) : R₁ × R₂) := fun h ↦ not_isUnit_zero (M₀ := R₂) (by simpa using h.map (RingHom.fst R₁ R₂))
  not_isLocalRing_def ha hb (by simp)

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