Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-04-08 12:50 5f1329a2

View on Github →

feat(linear_algebra/dual): add dual vector spaces (#881)

  • feat(linear_algebra/dual): add dual vector spaces Define dual modules and vector spaces and prove the basic theorems: the dual basis isomorphism and evaluation isomorphism in the finite dimensional case, and the corresponding (injectivity) statements in the general case. A variant of linear_map.ker_eq_bot and the "inverse" of is_basis.repr_total are included. Universe issues make an adaptation of linear_equiv.dim_eq necessary.
  • style(linear_algebra/dual): adapt to remarks from PR dsicussion
  • style(linear_algebra/dual): reformat proof of ker_eq_bot'

Estimated changes

added theorem linear_map.ker_eq_bot'
added theorem is_basis.repr_total
added theorem is_basis.dual_dim_eq
added def is_basis.to_dual
added theorem is_basis.to_dual_apply
added theorem is_basis.to_dual_inj
added theorem is_basis.to_dual_ker
added theorem is_basis.to_dual_range
added def module.dual.eval
added theorem module.dual.eval_apply
added def module.dual
added theorem vector_space.eval_ker