Theorems · Theorem · general topology

RestrictedProduct.single_mul

∀ {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [inst : (i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i)
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → MulZeroClass (G i)] [inst_3 : ∀ (i : ι), ZeroMemClass (S i) (G i)]
  [inst_4 : ∀ (i : ι), MulMemClass (S i) (G i)] (i : ι) (r : G i)
  (x : RestrictedProduct (fun i => G i) (fun i => ↑(A i)) Filter.cofinite),
  RestrictedProduct.single A i (r * x i) = RestrictedProduct.single A i r * x

Defined in

Mathlib.Topology.Algebra.RestrictedProduct.Basic

Cited by

0 results in Mathlib

Foundations

Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SetLikeDecidableEqMulZeroClassZeroMemClassMulMemClass