instIsReducedProd — Mathlib

English

The product of two reduced rings is reduced; in particular, if R and S are reduced, then R×S is reduced.

Русский

Произведение двух редуцированных колец редуцировано; если R и S редуцированы, то R×S тоже редуцированно.

LaTeX

$$$\\text{IsReduced }R \\land \\text{IsReduced }S \\Rightarrow \\text{IsReduced }(R \\times S)$$$

Lean4

instance [Zero R] [Pow R ℕ] [Zero S] [Pow S ℕ] [IsReduced R] [IsReduced S] : IsReduced (R × S) where
  eq_zero
    _ := fun ⟨n, hn⟩ ↦
    have hn := Prod.ext_iff.1 hn
    Prod.ext (IsReduced.eq_zero _ ⟨n, hn.1⟩) (IsReduced.eq_zero _ ⟨n, hn.2⟩)

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