Commit 2023-08-13 21:09 4fa9d3db

View on Github →

feat(LinearAlgebra/Basis): add lemmas/golf (#6460)

  • Add Basis.mem_span_image, Basis.self_mem_span_image.
  • Golf some proofs.
  • Add @[simp] to Basis.span_eq.

Estimated changes

added theorem Basis.mem_span_image
modified theorem Basis.mem_span_repr_support