mathlib3

ee0c179c - feat(number_theory/number_field/norm): add file (#17672)

feat(number_theory/number_field/norm): add file (#17672) We add `norm' : (𝓞 L) →* (𝓞 K)`, that is `algebra.norm K` as a morphism between the rings of integers. From flt-regular