mathlib3

b5dd709b - feat(analysis/inner_product_space/basic): Pythagoras with square roots (#17025)

feat(analysis/inner_product_space/basic): Pythagoras with square roots (#17025) Add two further variants of Pythagoras, expressed in terms of a norm equal to a square root instead of an expression for a square of a norm.