mathlib
a0ff65df - feat(ring_theory/norm): add is_integral_norm (#11489)

Commit

3 years ago

feat(ring_theory/norm): add is_integral_norm (#11489) We add `is_integral_norm`. From flt-regular

Author

riccardobrasca

Parents