Theorems · Theorem · ring theory

LinearMap.intrinsicStar_comp

∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring R] [inst_1 : InvolutiveStar R]
  [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : StarAddMonoid E] [inst_5 : StarModule R E]
  [inst_6 : AddCommMonoid F] [inst_7 : Module R F] [inst_8 : StarAddMonoid F] [inst_9 : StarModule R F] {G : Type u_4}
  [inst_10 : AddCommMonoid G] [inst_11 : Module R G] [inst_12 : StarAddMonoid G] [inst_13 : StarModule R G]
  (f : WithConv (E →ₗ[R] F)) (g : WithConv (G →ₗ[R] E)),
  star (WithConv.toConv (f.ofConv ∘ₗ g.ofConv)) = WithConv.toConv ((star f).ofConv ∘ₗ (star g).ofConv)

Defined in

Mathlib.Algebra.Star.LinearMap

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemiringInvolutiveStarAddCommMonoidModuleStarAddMonoidStarModuleAddCommMonoidModuleStarAddMonoidStarModuleAddCommMonoidModuleStarAddMonoidStarModule