sorry_proof
R : Type u_1
K : Type u_2
X : Type u_3
Y : Type u_4
inst✝³ : Scalar R K
inst✝² : AddCommMonoid K
inst✝¹ : Inner K X
inst✝ : Inner K Y
x : X
y : Y
⊢ ‖(x, y)‖₂ = Scalar.sqrt (‖x‖₂² + ‖y‖₂²)
no goals