Theorems · Definition · linear algebra

Module.Dual.eval

(R : Type u_1) →
  (M : Type u_3) →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → M →ₗ[R] Module.Dual R (Module.Dual R M)

Maps a module M to the dual of the dual of M. See Module.erange_coe and Module.evalEquiv.

Defined in

Mathlib.LinearAlgebra.Dual.Defs

Cited by

52 results in Mathlib

Foundations

Depth 35 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringAddCommMonoidModule