instMulCoeOfMulMemClass — Mathlib

English

If 𝓕 ≤ 𝓖, the restricted product with respect to 𝓖 naturally includes into the restricted product with respect to 𝓕.

Русский

Если 𝓕 ≤ 𝓖, ограниченное произведение по 𝓖 естественно включается в ограниченное произведение по 𝓕.

LaTeX

$$$\\mathrm{inclusion}(h)(x): \\mathrm{RestrictedProduct}_{𝓖} \\to \\mathrm{RestrictedProduct}_{𝓕}.$$$

Lean4

@[to_additive]
instance [Π i, Mul (R i)] [∀ i, MulMemClass (S i) (R i)] : Mul (Πʳ i, [R i, B i]_[𝓕]) where
  mul x y := ⟨fun i ↦ x i * y i, y.2.mp (x.2.mono fun _ ↦ mul_mem)⟩

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