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

State before:
R : Type u_1
inst✝ : RealScalar R
x : R
⊢ ‖x‖₂[R] = Scalar.abs x
Tactic:
sorry_proof
State after:
no goals