Mathlib Map

Structures · Lean core

SMul

Typeclass for types with a scalar multiplication operation, denoted • (\bu)

Defined in
Init.Prelude
Shape
2 explicit arguments · adds smul
Open in Mathlib docs

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by4

Forgetful instances

Every SMul is also a

Provided automatically by

Concrete types that are instances45

  • Int
  • Nat
  • Real
  • Rat
  • Quiver.Hom
  • NNReal
  • ZMod
  • Filter.Germ
  • BoundedContinuousFunction
  • NNRat
  • WithVal
  • HahnSeries
  • DomMulAct
  • Units
  • DirectSum
  • ContMDiffMap
  • OreLocalization
  • ArithmeticFunction
  • AdicCompletion
  • Matrix.SpecialLinearGroup
  • RingCat.carrier
  • IncidenceAlgebra
  • Polynomial.Gal
  • Circle
  • CategoryTheory.Aut
  • ConjAct
  • GrpCat.carrier
  • RegularWreathProduct
  • OrderIso
  • WeierstrassCurve.VariableChange
  • GradedMonoid
  • CategoryTheory.CatCenter
  • Subtype
  • OrderDual
  • Set.Elem
  • ULift
  • MulOpposite
  • PUnit
  • Lex
  • HasQuotient.Quotient
  • ContinuousMap
  • WithAbs
  • Colex
  • Multiplicative
  • Submodule

How is a type an instance?

Loading the hierarchy index…

Assumed by2,586

Ancestors3