Theorems · Theorem · Lie groups

RestrictedProduct.unitsEquiv_apply

∀ {ι : Type u_1} {R : ι → Type u_2} [inst : (i : ι) → Monoid (R i)] {S : ι → Type u_3}
  [inst_1 : (i : ι) → SetLike (S i) (R i)] [inst_2 : ∀ (i : ι), SubmonoidClass (S i) (R i)] {B : (i : ι) → S i}
  {𝓕 : Filter ι} (i : ι) (x : (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕)ˣ),
  ↑(((RestrictedProduct.unitsEquiv R) x) i) = ↑x i

Defined in

Mathlib.Topology.Algebra.RestrictedProduct.Units

Cited by

0 results in Mathlib

Foundations

Depth 30 from the axioms · uses propext, Quot.sound

Assumes

MonoidSetLikeSubmonoidClass