basic): notation for `with_zero (multiplicative ℤ)` (#14064)

Commit

3 years ago

feat(ring_theory/valuation/basic): notation for `with_zero (multiplicative ℤ)` (#14064) And likewise for `with_zero (multiplicative ℕ)`

Author

ocfnash

Parents