Theorem Submodule.exists_dual_map_eq_bot_of_lt_top

Modification history

2025-12-26 15:30
Mathlib/LinearAlgebra/Dual/Lemmas.lean
feat(LinearAlgebra/Dual/Lemmas): generalize hypotheses (#33101) …
Modified Submodule.exists_dual_map_eq_bot_of_lt_topView on Github →
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 →