Theorems · Theorem · linear algebra

Module.eval_ker

∀ (K : Type uK) (V : Type uV) [inst : CommSemiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [Module.Projective K V], (Module.Dual.eval K V).ker = ⊥

Defined in

Mathlib.LinearAlgebra.Dual.Lemmas

Cited by

2 results in Mathlib

Foundations

Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringAddCommMonoidModuleModule.Projective