Theorem Submodule.exists_dual_map_eq_bot_of_nmem

Modification history

2023-11-30 11:39
Mathlib/LinearAlgebra/Dual.lean
feat: the annihilator of the kernel of the trace form of a Lie module is contained in the span of its weights (#8739)
Added Submodule.exists_dual_map_eq_bot_of_nmemView on Github →