instIsPrincipalIdealRingForallOfFinite

English

The finite product of principal ideal rings is a principal ideal ring: if the index set ι is finite and each R_i is principal, then the product ∏_i R_i is principal.

Русский

Конечный прямой произведение колец, каждый из которых главен, является главейколь идеал-рингом.

LaTeX

$$$[\text{Finite } \iota] [\forall i, \mathrm{IsPrincipalIdealRing}(R_i)] \Rightarrow \mathrm{IsPrincipalIdealRing}(\prod_{i} R_i)$$$

Lean4

instance [Finite ι] [∀ i, IsPrincipalIdealRing (R i)] : IsPrincipalIdealRing (Π i, R i) where
  principal
    I := by
    rw [← piOrderIso.symm_apply_apply I]
    exact ⟨_, congr(pi $(funext fun i ↦ (Submodule.IsPrincipal.span_singleton_generator _).symm)).trans pi_span⟩

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