Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-22 06:29 49ce9677

View on Github →

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

Estimated changes

Modified src/number_theory/function_field.lean

modified def function_field.infty_valuation

modified def function_field.infty_valuation_def

modified def function_field.infty_valued_Fqt

Modified src/ring_theory/dedekind_domain/adic_valuation.lean

modified def is_dedekind_domain.height_one_spectrum.adic_valued

modified def is_dedekind_domain.height_one_spectrum.int_valuation

modified def is_dedekind_domain.height_one_spectrum.int_valuation_def

modified def is_dedekind_domain.height_one_spectrum.valuation

Modified src/ring_theory/valuation/basic.lean