Def module.dual
Modification history
2023-05-07 21:39
src/linear_algebra/dual.lean
refactor(linear_algebra/dual): make `module.dual` reducible (#18963) …
Added module.dualView on Github →2019-10-01 18:48
src/linear_algebra/dual.lean
feat(tactic/delta_instance): handle parameters and use in library (#1483) …
Deleted module.dualView on Github →2019-04-08 12:50
src/linear_algebra/dual.lean
feat(linear_algebra/dual): add dual vector spaces (#881) …
Added module.dualView on Github →2017-11-10 11:32
algebra/module.lean
chore(algebra/module): hide ring parameters, vector_space is no a proper class, remove dual, change variables to implicits …
Deleted module.dualView on Github →