Theorems · Inductive type · ring theory

StarAlgEquiv

(R : Type u_1) →
  (A : Type u_2) →
    (B : Type u_3) →
      [Add A] → [Add B] → [Mul A] → [Mul B] → [SMul R A] → [SMul R B] → [Star A] → [Star B] → Type (max u_2 u_3)

A ⋆-algebra equivalence is an equivalence preserving addition, multiplication, scalar multiplication and the star operation, which allows for considering both unital and non-unital equivalences with a single structure.

Defined in

Mathlib.Algebra.Star.StarAlgHom

Cited by

132 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 5 definitions · uses no axioms

Assumes

AddAddMulMulSMulSMulStarStar