Theorems · Theorem · ring theory

StarAlgEquiv.ofNonUnitalStarAlgHom_apply

∀ {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A₁]
  [inst_2 : DistribMulAction R A₁] [inst_3 : Star A₁] [inst_4 : NonUnitalNonAssocSemiring A₂]
  [inst_5 : DistribMulAction R A₂] [inst_6 : Star A₂] (f : A₁ →⋆ₙₐ[R] A₂) (g : A₂ →⋆ₙₐ[R] A₁)
  (h₁ : g.comp f = NonUnitalStarAlgHom.id R A₁) (h₂ : f.comp g = NonUnitalStarAlgHom.id R A₂) (a : A₁),
  (StarAlgEquiv.ofNonUnitalStarAlgHom f g h₁ h₂) a = f a

Defined in

Mathlib.Algebra.Star.StarAlgHom

Cited by

0 results in Mathlib

Foundations

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

Assumes

MonoidNonUnitalNonAssocSemiringDistribMulActionStarNonUnitalNonAssocSemiringDistribMulActionStar