feat(ring_theory): define the field/algebra norm (#7636)
This PR defines the field norm `algebra.norm K L : L →* K`, where `L` is a finite field extension of `K`. In fact, it defines this for any `algebra R S` instance, where `R` and `S` are integral domains. (With a default value of `1` if `S` does not have a finite `R`-basis.)
The approach is to basically copy `ring_theory/trace.lean` and replace `trace` with `det` or `norm` as appropriate.
