Theorems · Theorem · linear algebra

Module.Dual.eval_apply

∀ (R : Type u_1) (M : Type u_3) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (v : M)
  (a : Module.Dual R M), ((Module.Dual.eval R M) v) a = a v

Defined in

Mathlib.LinearAlgebra.Dual.Defs

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModule