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.







leanprover-community/mathlib,leanprover-community/mathlib