Mathlib Map

Theorems · Definition · ring theory

Module.End.smulLeft

{R : Type u_1} →
  {M : Type u_4} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (α : R) → α ∈ Set.center R → Module.End R M

Scalar multiplication on the left, as a linear map.

Defined in
Mathlib.Algebra.Module.LinearMap.End
Cited by
8 results in Mathlib
Foundations
Depth 17 from the axioms · uses propext
Assumes
SemiringAddCommMonoidModule
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Module.End.mem_center_iff · cited by 4End.mem_center_iffLieDerivation.ofGradingSum · cited by 2LieDerivation.ofGradingSumModule.End.smulLeft_apply · cited by 1End.smulLeft_applyModule.End.smulLeft.congr_simp · cited by 0smulLeft.congr_simpModule.End.smulLeft_eq · cited by 0End.smulLeft_eqModule.End.mem_subalgebraCenter_iff · cited by 0End.mem_subalgebraCenter_…Module.End.mem_submonoidCenter_iff · cited by 0End.mem_submonoidCenter_i…Module.End.mem_subsemigroupCenter_iff · cited by 0End.mem_subsemigroupCente…Module.End.mem_subsemiringCenter_iff · cited by 0End.mem_subsemiringCenter…Set · cited by 53352SetModule · cited by 20661ModuleSemiring · cited by 13802SemiringAddCommMonoid · cited by 12281AddCommMonoidModule.End · cited by 774Module.EndSet.center · cited by 49Set.centerEnd.smulLeftCITED BYCITES

Cites6

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

  • Setstatement · cited by 53,352
  • Modulestatement and proof · cited by 20,661
  • Semiringstatement and proof · cited by 13,802
  • AddCommMonoidstatement and proof · cited by 12,281
  • Module.Endstatement · cited by 774
  • Set.centerstatement and proof · cited by 49

Cited by9

Results whose statement or proof uses this declaration.