Theorems · Inductive type · commutative algebra
Module
(R : Type u) → (M : Type v) → [Semiring R] → [AddCommMonoid M] → Type (max u v)
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
- Cited by
- 20,661 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 3 definitions · uses no axioms
- Assumes
- SemiringAddCommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement · cited by 13,802
- AddCommMonoidstatement · cited by 12,281
Cited by24,942
Results whose statement or proof uses this declaration.
- LinearMapstatement · cited by 10,215
- Submodulestatement · cited by 7,192
- ContinuousLinearMapstatement · cited by 5,352
- LinearEquivstatement · cited by 3,317
- TensorProductstatement and proof · cited by 2,545
- FiniteDimensionalstatement and proof · cited by 1,854
- Module.finrankstatement and proof · cited by 1,770
- LinearMap.compstatement and proof · cited by 1,642
- Submodule.spanstatement and proof · cited by 1,504
- Module.Basisstatement · cited by 1,477
- LinearEquiv.symmstatement and proof · cited by 1,461
- TensorProduct.tmulstatement and proof · cited by 1,182
Showing the 200 most cited of 24,942.