feat(ring_theory/norm): add norm_norm (#18860)
Prove the transitivity of the algebra.norm
```lean
lemma algebra.norm_norm [is_scalar_tower K L F] [finite_dimensional K F] [is_separable K F] (x : F) :
norm K (norm L x) = norm K x
```
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
