Theorems · Definition · Lie groups

RestrictedProduct.unitsEquiv

{ι : 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 ι} →
                (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕)ˣ ≃*
                  RestrictedProduct (fun i => (R i)ˣ) (fun i => ↑(Submonoid.ofClass (B i)).units) 𝓕

The ring isomorphism between the units of a restricted product Πʳ i, [R i, B i]_[𝓕] and the restricted product of (R i)ˣ with respect to (B i)ˣ.

Defined in

Mathlib.Topology.Algebra.RestrictedProduct.Units

Cited by

3 results in Mathlib

Foundations

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

Assumes

MonoidSetLikeSubmonoidClass