Theorems · Theorem · ring theory

StarAlgEquiv.restrictScalars_symm_apply

∀ (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : MulAction R S]
  [inst_5 : Module S A] [inst_6 : Module S B] [inst_7 : Module R A] [inst_8 : Module R B] [inst_9 : IsScalarTower R S A]
  [inst_10 : IsScalarTower R S B] [inst_11 : Star A] [inst_12 : Star B] (f : A ≃⋆ₐ[S] B) (a : B),
  (StarAlgEquiv.restrictScalars R f).symm a = f.invFun a

Defined in

Mathlib.Algebra.Star.Subalgebra

Cited by

0 results in Mathlib

Foundations

Depth 27 from the axioms · uses Quot.sound

Assumes

CommSemiringCommSemiringNonUnitalNonAssocSemiringNonUnitalNonAssocSemiringMulActionModuleModuleModuleModuleIsScalarTowerIsScalarTowerStarStar