Mathlib Map

Theorems · Theorem · ring theory

StarModule.star_smul

∀ {R : Type u} {A : Type v} {inst : Star R} {inst_1 : Star A} {inst_2 : SMul R A} [self : StarModule R A] (r : R)
  (a : A), star (r • a) = star r • star a

star commutes with scalar multiplication

Defined in
Mathlib.Algebra.Star.Basic
Cited by
34 results in Mathlib
Foundations
Depth 4 from the axioms · uses no axioms
Assumes
StarModule
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

IsSelfAdjoint.smul · cited by 7IsSelfAdjoint.smulMatrix.conjTranspose_smul · cited by 5Matrix.conjTranspose_smulrealPart_I_smul · cited by 4realPart_I_smulinner_smul_right_eq_smul · cited by 3inner_smul_right_eq_smulalgebraMap_star_comm · cited by 3algebraMap_star_commimaginaryPart_I_smul · cited by 2imaginaryPart_I_smulCStarModule.inner_smul_left_complex · cited by 2CStarModule.inner_smul_le…CStarModule.inner_smul_left_real · cited by 2CStarModule.inner_smul_le…IsSelfAdjoint.smul_mem_skewAdjoint · cited by 2IsSelfAdjoint.smul_mem_sk…CFC.abs_smul_nonneg · cited by 2CFC.abs_smul_nonnegisSelfAdjoint_smul_of_mem_skewAdjoint · cited by 1isSelfAdjoint_smul_of_mem…Function.Injective.starModule · cited by 1Injective.starModuleCStarModule.inner_smul_right_real · cited by 1CStarModule.inner_smul_ri…Unitary.smul_mem_of_mem · cited by 1Unitary.smul_mem_of_memstar_mul_self_add_self_mul_star · cited by 1star_mul_self_add_self_mu…Star.star · cited by 1082Star.starStarModule · cited by 570StarModuleStar · cited by 496StarStarModule.star_smulCITED BYCITES

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Star.starstatement · cited by 1,082
  • StarModulestatement and proof · cited by 570
  • Starstatement and proof · cited by 496

Cited by34

Results whose statement or proof uses this declaration.