Commit 2025-12-26 15:30 3a194f78

View on Github →

feat(LinearAlgebra/Dual/Lemmas): generalize hypotheses (#33101) Generalize a few lemmas to either

a noncommutative setting
a Module.Free hypothesis in an instance is replaced by the corresponding Module.Projective.

Estimated changes

Modified Mathlib/LinearAlgebra/Dual/Lemmas.lean

modified theorem Module.Dual.range_eq_top_of_ne_zero

modified theorem Module.forall_dual_apply_eq_zero_iff

modified theorem Submodule.exists_dual_map_eq_bot_of_lt_top

modified theorem Submodule.exists_dual_map_eq_bot_of_notMem