English
The polynomial ring over a finite product of rings is isomorphic to the product of polynomial rings over each factor: (∏ R_i)[X] ≃ ∏ (R_i[X]).
Русский
Полином кольцо над конечным произведением колец изоморфно произведению полиномов над каждым фактором: (∏ R_i)[X] ≃ ∏ (R_i[X]).
LaTeX
$$$\\bigl(\\prod_{i} R_i\\bigr)[X] \\cong \\prod_{i} (R_i[X])$$$
Lean4
/-- The polynomial ring over a finite product of rings is isomorphic to
the product of polynomial rings over individual rings. -/
def piEquiv {ι} [Finite ι] (R : ι → Type*) [∀ i, Semiring (R i)] : (∀ i, R i)[X] ≃+* ∀ i, (R i)[X] :=
.ofBijective (Pi.ringHom fun i ↦ mapRingHom (Pi.evalRingHom R i))
⟨fun p q h ↦ by ext n i; simpa using congr_arg (fun p ↦ coeff (p i) n) h, fun p ↦
⟨.ofFinsupp
(.ofSupportFinite (fun n i ↦ coeff (p i) n) <|
(Set.finite_iUnion fun i ↦ (p i).support.finite_toSet).subset fun n hn ↦
by
simp only [Set.mem_iUnion, Finset.mem_coe, mem_support_iff, Function.mem_support] at hn ⊢
contrapose! hn; exact funext hn),
by ext i n; exact coeff_map _ _⟩⟩
