Commit 2023-01-27 17:10 5fe29816

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