Theorem: SciLean.norm₂_prod (SciLean/Core/Objects/SemiInnerProductSpace.lean)

State before:
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‖₂²)
Tactic:
sorry_proof
State after:
no goals