Theorems · Definition · ring theory

Unitary.mapEquiv

{R : Type u_2} →
  {S : Type u_3} →
    [inst : Monoid R] →
      [inst_1 : StarMul R] → [inst_2 : Monoid S] → [inst_3 : StarMul S] → (R ≃⋆* S) → ↥(unitary R) ≃⋆* ↥(unitary S)

The star monoid isomorphism between unitary subgroups induced by a star monoid isomorphism of the underlying star monoids.

Defined in

Mathlib.Algebra.Star.Unitary

Cited by

6 results in Mathlib

Foundations

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

Assumes

MonoidStarMulMonoidStarMul