Theorem Submodule.exists_dual_map_eq_bot_of_notMem

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_notMemView on Github →
2025-05-25 12:30
Mathlib/LinearAlgebra/Dual/Lemmas.lean
chore(*): not_mem/nmem -> notMem (#25159)
Added Submodule.exists_dual_map_eq_bot_of_notMemView on Github →