mathlib3
e61db52e - chore(linear_algebra/quadratic_form): add polar_self, polar_zero_left, and polar_zero_right simp lemmas (#6003)
Commit
View On GitHub
Commit
5 years ago
chore(linear_algebra/quadratic_form): add polar_self, polar_zero_left, and polar_zero_right simp lemmas (#6003) This also reorders the existing lemmas to keep the polar ones separate from the non-polar ones
Author
eric-wieser eric-wieser
Parents
1a2eb0b5
FAQ Terms Privacy Refunds Impressum
Loading