isPrincipalIdealRing_prod_iff — Mathlib

English

IsPrincipalIdealRing (R × S) if and only if IsPrincipalIdealRing R and IsPrincipalIdealRing S.

Русский

IsPrincipalIdealRing (R × S) эквивалентно IsPrincipalIdealRing R и IsPrincipalIdealRing S.

LaTeX

$$$IsPrincipalIdealRing(R \\times S) \\\\iff (IsPrincipalIdealRing R \\\\land IsPrincipalIdealRing S)$$$

Lean4

theorem isPrincipalIdealRing_prod_iff : IsPrincipalIdealRing (R × S) ↔ IsPrincipalIdealRing R ∧ IsPrincipalIdealRing S
    where
  mp h := ⟨h.of_surjective (RingHom.fst R S) Prod.fst_surjective, h.of_surjective (RingHom.snd R S) Prod.snd_surjective⟩
  mpr := fun ⟨_, _⟩ ↦ inferInstance

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