Theorem Submodule.coe_dualAnnihilator_span

Modification history

2025-03-07 22:53
Mathlib/LinearAlgebra/Dual/Defs.lean
chore(LinearAlgebra): split long file `Dual.lean` (#22697) …
Modified Submodule.coe_dualAnnihilator_spanView on Github →
2024-11-07 11:59
Mathlib/LinearAlgebra/Dual.lean
feat: define restrictions of perfect pairings (#18559) …
Added Submodule.coe_dualAnnihilator_spanView on Github →