Commit 2021-09-10 10:53 a057a8e9
View on Github →feat(ring_theory/norm): norm R x = 0 ↔ x = 0 (#9042)
Nonzero values of S / R have nonzero norm over R.
feat(ring_theory/norm): norm R x = 0 ↔ x = 0 (#9042)
Nonzero values of S / R have nonzero norm over R.