Theorems · Definition · ring theory

Unitary.conjStarAlgAut

(S : Type u_1) →
  (R : Type u_2) →
    [inst : Semiring R] →
      [inst_1 : StarMul R] →
        [inst_2 : SMul S R] → [IsScalarTower S R R] → [SMulCommClass S R R] → ↥(unitary R) →* R ≃⋆ₐ[S] R

Each unitary element u defines a ⋆-algebra automorphism such that x ↦ u * x * star u. This is the ⋆-algebra automorphism version of a specialized version of MulSemiringAction.toAlgAut.

Defined in

Mathlib.Algebra.Star.UnitaryStarAlgAut

Cited by

26 results in Mathlib

Foundations

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

Assumes

SemiringStarMulSMulIsScalarTowerSMulCommClass