mathlib3
feat(inner_product_space/positive): matrix.pos_semidef iff x.to_euclidean_lin.is_positive
#18786
Open
Overview
Commits
10
Changes
View On GitHub
Commits
  • chore(inner_product_space/positive): some lemmas
    themathqueen committed 3 years ago
  • fix
    themathqueen committed 3 years ago
  • changes after review
    themathqueen committed 3 years ago
  • fix
    themathqueen committed 3 years ago
  • Merge branch 'master' into inner_product_space_positive
    eric-wieser committed 3 years ago
  • delete pairwise_orthogonal
    eric-wieser committed 3 years ago
  • fixes
    themathqueen committed 3 years ago
  • change name and remove lemma
    themathqueen committed 3 years ago
  • move results to new pr
    themathqueen committed 3 years ago
  • feat(inner_product_space/positive): matrix.pos_semidef iff x.to_euclidean_lin.is_positive
    themathqueen committed 3 years ago
FAQ Terms Privacy Refunds Impressum
Loading