mathlib

19534b29 - feat(analysis/inner_product_space/basic) : `inner_map_self_eq_zero` (#12065)

feat(analysis/inner_product_space/basic) : `inner_map_self_eq_zero` (#12065) The main result here is: If ⟪T x, x⟫_C = 0 for all x, then T = 0. The proof uses a polarization identity. Note that this is false with R in place of C. I am confident that my use of ring_nf is not optimal, but I hope to learn from the cleanup process! Co-authored-by: Daniel Packer Co-authored-by: Hans Parshall <hparshall@users.noreply.github.com>