feat(ring_theory/valuation/basic): notation for `with_zero (multiplic…

…ative ℤ)` (#14064)

And likewise for `with_zero (multiplicative ℕ)`

src/number_theory/function_field.lean

@@ -40,7 +40,7 @@ function field, ring of integers
 -/
 
 noncomputable theory
-open_locale non_zero_divisors polynomial
+open_locale non_zero_divisors polynomial discrete_valuation
 
 variables (Fq F : Type) [field Fq] [field F]
 
@@ -148,7 +148,7 @@ variable [decidable_eq (ratfunc Fq)]
 /-- The valuation at infinity is the nonarchimedean valuation on `Fq(t)` with uniformizer `1/t`.
 Explicitly, if `f/g ∈ Fq(t)` is a nonzero quotient of polynomials, its valuation at infinity is
 `multiplicative.of_add(degree(f) - degree(g))`. -/
-def infty_valuation_def (r : ratfunc Fq) : with_zero (multiplicative ℤ) :=
+def infty_valuation_def (r : ratfunc Fq) : ℤₘ₀ :=
 if r = 0 then 0 else (multiplicative.of_add r.int_degree)
 
 lemma infty_valuation.map_zero' : infty_valuation_def Fq 0 = 0 := if_pos rfl
@@ -197,7 +197,7 @@ end
 by rw [infty_valuation_def, if_neg hx]
 
 /-- The valuation at infinity on `Fq(t)`. -/
-def infty_valuation  : valuation (ratfunc Fq) (with_zero (multiplicative ℤ)) :=
+def infty_valuation  : valuation (ratfunc Fq) ℤₘ₀ :=
 { to_fun          := infty_valuation_def Fq,
   map_zero'       := infty_valuation.map_zero' Fq,
   map_one'        := infty_valuation.map_one' Fq,
@@ -228,7 +228,7 @@ begin
 end
 
 /-- The valued field `Fq(t)` with the valuation at infinity. -/
-def infty_valued_Fqt : valued (ratfunc Fq) (with_zero (multiplicative ℤ)) :=
+def infty_valued_Fqt : valued (ratfunc Fq) ℤₘ₀ :=
 valued.mk' $ infty_valuation Fq
 
 lemma infty_valued_Fqt.def {x : ratfunc Fq} :
@@ -246,7 +246,7 @@ end
 instance : inhabited (Fqt_infty Fq) := ⟨(0 : Fqt_infty Fq)⟩
 
 /-- The valuation at infinity on `k(t)` extends to a valuation on `Fqt_infty`. -/
-instance valued_Fqt_infty : valued (Fqt_infty Fq) (with_zero (multiplicative ℤ)) :=
+instance valued_Fqt_infty : valued (Fqt_infty Fq) ℤₘ₀ :=
 @valued.valued_completion _ _ _ _ (infty_valued_Fqt Fq)
 
 lemma valued_Fqt_infty.def {x : Fqt_infty Fq} :

src/ring_theory/dedekind_domain/adic_valuation.lean

@@ -57,7 +57,7 @@ dedekind domain, dedekind ring, adic valuation
 -/
 
 noncomputable theory
-open_locale classical
+open_locale classical discrete_valuation
 
 open multiplicative is_dedekind_domain
 
@@ -70,7 +70,7 @@ namespace is_dedekind_domain.height_one_spectrum
 /-- The additive `v`-adic valuation of `r ∈ R` is the exponent of `v` in the factorization of the
 ideal `(r)`, if `r` is nonzero, or infinity, if `r = 0`. `int_valuation_def` is the corresponding
 multiplicative valuation. -/
-def int_valuation_def (r : R) : with_zero (multiplicative ℤ) :=
+def int_valuation_def (r : R) : ℤₘ₀ :=
 if r = 0 then 0 else multiplicative.of_add
   (-(associates.mk v.as_ideal).count (associates.mk (ideal.span {r} : ideal R)).factors : ℤ)
 
@@ -207,7 +207,7 @@ begin
 end
 
 /-- The `v`-adic valuation on `R`. -/
-def int_valuation : valuation R (with_zero (multiplicative ℤ)) :=
+def int_valuation : valuation R ℤₘ₀ :=
 { to_fun          := v.int_valuation_def,
   map_zero'       := int_valuation.map_zero' v,
   map_one'        := int_valuation.map_one' v,
@@ -243,7 +243,7 @@ end
 
 /-- The `v`-adic valuation of `x ∈ K` is the valuation of `r` divided by the valuation of `s`,
 where `r` and `s` are chosen so that `x = r/s`. -/
-def valuation (v : height_one_spectrum R) : valuation K (with_zero (multiplicative ℤ)) :=
+def valuation (v : height_one_spectrum R) : valuation K ℤₘ₀ :=
 v.int_valuation.extend_to_localization (λ r hr, set.mem_compl $ v.int_valuation_ne_zero' ⟨r, hr⟩) K
 
 lemma valuation_def (x : K) : v.valuation x = v.int_valuation.extend_to_localization
@@ -303,7 +303,7 @@ ring of integers, denoted `v.adic_completion_integers`. -/
 variable {K}
 
 /-- `K` as a valued field with the `v`-adic valuation. -/
-def adic_valued : valued K (with_zero (multiplicative ℤ)) := valued.mk' v.valuation
+def adic_valued : valued K ℤₘ₀ := valued.mk' v.valuation
 
 lemma adic_valued_apply {x : K} : (v.adic_valued.v : _) x = v.valuation x := rfl
 
@@ -317,7 +317,7 @@ instance : field (v.adic_completion K) :=
 
 instance : inhabited (v.adic_completion K) := ⟨0⟩
 
-instance valued_adic_completion : valued (v.adic_completion K) (with_zero (multiplicative ℤ)) :=
+instance valued_adic_completion : valued (v.adic_completion K) ℤₘ₀ :=
 @valued.valued_completion _ _ _ _ v.adic_valued
 
 lemma valued_adic_completion_def {x : v.adic_completion K} :

src/ring_theory/valuation/basic.lean

@@ -49,6 +49,13 @@ on R / J = `ideal.quotient J` is `on_quot v h`.
 
 `add_valuation R Γ₀` is implemented as `valuation R (multiplicative Γ₀)ᵒᵈ`.
 
+## Notation
+
+In the `discrete_valuation` locale:
+
+ * `ℕₘ₀` is a shorthand for `with_zero (multiplicative ℕ)`
+ * `ℤₘ₀` is a shorthand for `with_zero (multiplicative ℤ)`
+
 ## TODO
 
 If ever someone extends `valuation`, we should fully comply to the `fun_like` by migrating the
@@ -743,3 +750,10 @@ end supp -- end of section
 attribute [irreducible] add_valuation
 
 end add_valuation
+
+section valuation_notation
+
+localized "notation `ℕₘ₀` := with_zero (multiplicative ℕ)" in discrete_valuation
+localized "notation `ℤₘ₀` := with_zero (multiplicative ℤ)" in discrete_valuation
+
+end valuation_notation