feat: final lemmas needed for showing gaussNorm on MvPowerSeries is an absolute value (#40997)

We finish our section on showing that the gaussNorm on MvRestricted power series will be an absolute value by giving the neg and mul_eq_mul lemmas.

Co-authored-by: WilliamCoram <williamecoram@gmail.com>

Author: WilliamCoram

Mathlib/RingTheory/MvPowerSeries/GaussNorm.lean

@@ -33,6 +33,13 @@ the set of all values of `v (coeff t f) * ∏ i : t.support, c i` for all `t : 
 * `MvPowerSeries.gaussNorm_add_le_max`: if `v` is a non-negative non-archimedean function and the
   set of values `v (coeff t f) * ∏ i : t.support, c i` is bounded above (similarly for `g`), then
   the Gauss norm has the non-archimedean property.
+
+* `MvPowerSeries.AchievesGaussNorm`: a type `i` is said to achieve gauss norm if
+  `v (coeff i f) * i.prod (c · ^ ·) = gaussNorm v c f`.
+
+* `MvPowerSeries.gaussNorm_neg`: if `v` has the property that `∀ i, v i = v (-i)` then
+  `gaussNorm v c (-f) = gaussNorm v c f `.
+
 -/
 
 @[expose] public section
@@ -164,6 +171,12 @@ variable [Ring R]
 abbrev AchievesGaussNorm (i : σ →₀ ℕ) : Prop :=
   v (coeff i f) * i.prod (c · ^ ·) = gaussNorm v c f
 
+lemma gaussNorm_neg (vNeg : ∀ x, v (-x) = v x) (f : MvPowerSeries σ R) :
+    gaussNorm v c (-f) = gaussNorm v c f  := by
+  simp_rw [gaussNorm]
+  have (t : σ →₀ ℕ) : (coeff t) (-f) = - (coeff t) f := by rfl
+  simp_rw [this, vNeg]
+
 section absoluteValue
 
 variable {α S : Type*} [LinearOrder S] [AddCommGroup α] (f : α → S)
@@ -226,6 +239,30 @@ lemma gaussNorm_le_mul (vMulEq : ∀ a b, v (a * b) = v a * v b)
       rw [antidiagonal_dominant v f g i₀ j₀ vna vMulEq vNeg hdom']
     _ ≤ gaussNorm v c (f * g) := le_gaussNorm v c (f * g) hbfg (i₀ + j₀)
 
+lemma gaussNorm_mul_eq_mul (f g : MvPowerSeries σ R) (hf : HasGaussNorm v c f)
+    (hg : HasGaussNorm v c g) (hfg : HasGaussNorm v c (f * g))
+    (vNonneg : ∀ a, v a ≥ 0) (vZero : v 0 = 0) (vNA : IsNonarchimedean v)
+    (vMulEq : ∀ (a b : R), v (a * b) = v a * v b) (vNeg : ∀ (a : R), v (-a) = v a)
+    (h_eq_zero : ∀ (x : R), v x = 0 → x = 0) (hc : ∀ (i : σ), 0 < c i)
+    (hdom : ∃ i j, AchievesGaussNorm v c f i ∧ AchievesGaussNorm v c g j ∧
+      ∀ p ∈ Finset.antidiagonal (i + j), p ≠ (i, j) → v (coeff p.1 f * coeff p.2 g) <
+      v (coeff i f) * v (coeff j g)) :
+    gaussNorm v c (f * g) = gaussNorm v c f * gaussNorm v c g := by
+  by_cases hf' : f = 0
+  · simp [hf', gaussNorm_zero v c vZero]
+  by_cases hg' : g = 0
+  · simp [hg', gaussNorm_zero v c vZero]
+  have hf1 : gaussNorm v c f ≠ 0 := by
+    convert gaussNorm_eq_zero_iff v c f vZero vNonneg h_eq_zero hc hf
+    grind
+  have hg1 : gaussNorm v c g ≠ 0 := by
+    convert gaussNorm_eq_zero_iff v c g vZero vNonneg h_eq_zero hc hg
+    grind
+  apply ge_antisymm_iff.mpr
+  constructor
+  · exact gaussNorm_le_mul v c f g vMulEq vNA (by grind) hfg hdom
+  · exact gaussNorm_mul_le v c f g (StrongLT.le hc) vNonneg (by grind) vNA vZero hf hg
+
 end absoluteValue
 
 end MvPowerSeries