mathlib3

121b699f - feat(ring_theory/norm): `norm R x = 0 ↔ x = 0`