instRingCoeOfSubringClass — Mathlib

English

If each fiber is a Ring and S_i is a Subring, the projection maps are injective via the coordinatewise embedding into the full product.

Русский

Если каждое волокно — кольцо и S_i — подкольцо, проекции инъективны через координатное вложение в полный произведение.

LaTeX

$$$ f: \text{RestrictedProduct} \to \prod_i R_i \quad \text{is injective on coordinatewise embedding}. $$$

Lean4

instance [Π i, Ring (R i)] [∀ i, SubringClass (S i) (R i)] : Ring (Πʳ i, [R i, B i]_[𝓕]) :=
  DFunLike.coe_injective.ring _ rfl rfl (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
    (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ ↦ rfl) (fun _ ↦ rfl)

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