feat(ring_theory): lemmas on algebra norm (#18298)
This PR includes some results on the algebra norm needed for the ideal norm:
* `algebra.norm R (0 : S) = 0` under weaker conditions on `R` and `S`
* use `module.free` and `module.finite` instead of explicit bases in `algebra.norm_eq_zero_iff` / generalize from vector spaces over a field to free modules over a ring
* the norm map between localizations is equal to the norm over the base fields
