Mathlib Map

Structures · Algebra

Module

A module is a generalization of vector spaces to a scalar semiring. It consists of a scalar semiring R and an additive monoid of "vectors" M, connected by a "scalar multiplication" operation r • x : M (where r : R and x : M) with some natural associativity and distributivity axioms similar to those on a ring.

Defined in
Mathlib.Algebra.Module.Defs
Shape
2 explicit arguments · adds add_smul, zero_smul
Open in Mathlib docs

Extends1

Extended by6

Concrete types that are instances43

  • Int
  • Nat
  • Real
  • Rat
  • Complex
  • NNReal
  • CategoryTheory.Functor.obj
  • ContinuousLinearMap
  • ZMod
  • Polynomial
  • Filter.Germ
  • BoundedContinuousFunction
  • CommRingCat.carrier
  • NNRat
  • TensorProduct
  • FractionRing
  • Matrix
  • WithVal
  • HahnSeries
  • DomMulAct
  • MonoidAlgebra
  • DirectSum
  • IsLocalRing.ResidueField
  • ContMDiffMap
  • OreLocalization
  • SetSemiring
  • CategoryTheory.End
  • ArithmeticFunction
  • AdicCompletion
  • Module.End
  • RingCat.carrier
  • CentroidHom
  • AddMonoid.End
  • IncidenceAlgebra
  • Subtype
  • OrderDual
  • ULift
  • MulOpposite
  • Lex
  • HasQuotient.Quotient
  • ContinuousMap
  • WithAbs
  • Ideal

How is a type an instance?

Loading the hierarchy index…

Assumed by24,684

Ancestors7