Theorems · Inductive type · ring theory

NonUnitalAlgEquivClass

(F : Type u_1) →
  (R : outParam (Type u_2)) →
    (A : outParam (Type u_3)) →
      (B : outParam (Type u_4)) →
        [Add A] → [Mul A] → [SMul R A] → [Add B] → [Mul B] → [SMul R B] → [EquivLike F A B] → Prop

The class that directly extends RingEquivClass and SMulHomClass. Mostly an implementation detail for the ⋆-algebra equivalence class which is currently: [NonUnitalAlgEquivClass] and [StarHomClass].

Defined in

Mathlib.Algebra.Star.StarAlgHom

Cited by

4 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

AddMulSMulAddMulSMulEquivLike