feat(ring_theory/norm): add is_integral_norm (#11489)
feat(ring_theory/norm): add is_integral_norm (#11489)

We add `is_integral_norm`.

From flt-regular





leanprover-community/mathlib,leanprover-community/mathlib