Theorems · Definition · linear algebra

Module.Dual

(R : Type u_4) → (M : Type u_5) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Type (max u_5 u_4)

The left dual space of an R-module M is the R-module of linear maps M → R.

Defined in

Mathlib.LinearAlgebra.Dual.Defs

Cited by

583 results in Mathlib

Foundations

Depth 14 from the axioms, rests on 143 definitions · uses no axioms

Assumes

SemiringAddCommMonoidModule