Theorem Submodule.exists_dual_map_eq_bot_of_lt_top

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_lt_topView on Github →