feat(ring_theory/hahn_series): introduce ring of Hahn series (#6237)

Defines Hahn series
Provides basic algebraic structure on Hahn series, up to `comm_ring`.

src/data/support.lean

@@ -7,6 +7,7 @@ import order.conditionally_complete_lattice
 import algebra.big_operators.basic
 import algebra.group.prod
 import algebra.group.pi
+import algebra.module.pi
 
 /-!
 # Support of a function
@@ -29,6 +30,7 @@ lemma nmem_support [has_zero A] {f : α → A} {x : α} :
   x ∉ support f ↔ f x = 0 :=
 not_not
 
+@[simp]
 lemma mem_support [has_zero A] {f : α → A} {x : α} :
   x ∈ support f ↔ f x ≠ 0 :=
 iff.rfl
@@ -74,6 +76,15 @@ support_binop_subset (has_sub.sub) (sub_self _) f g
 set.ext $ λ x, by simp only [support, ne.def, mul_eq_zero, mem_set_of_eq,
   mem_inter_iff, not_or_distrib]
 
+lemma support_smul_subset [add_monoid A] [monoid B] [distrib_mul_action B A]
+  (b : B) (f : α → A) :
+  support (b • f) ⊆ support f :=
+begin
+  simp_rw [support_subset_iff, mem_support],
+  refine λ x hbf hf, hbf _,
+  rw [pi.smul_apply, hf, smul_zero],
+end
+
 @[simp] lemma support_inv [division_ring A] (f : α → A) :
   support (λ x, (f x)⁻¹) = support f :=
 set.ext $ λ x, not_congr inv_eq_zero
@@ -156,3 +167,35 @@ set.ext $ λ x, by simp only [support, not_and_distrib, mem_union_eq, mem_set_of
   prod.mk_eq_zero, ne.def]
 
 end function
+
+namespace pi
+variables {A : Type*} {B : Type*} [decidable_eq A] [has_zero B] {a : A} {b : B}
+
+lemma support_single_zero : function.support (pi.single a (0 : B)) = ∅ := by simp
+
+@[simp]
+lemma support_single_of_ne (h : b ≠ 0) :
+  function.support (pi.single a b) = {a} :=
+begin
+  ext,
+  simp only [mem_singleton_iff, ne.def, function.mem_support],
+  split,
+  { contrapose!,
+    exact λ h', single_eq_of_ne h' b },
+  { rintro rfl,
+    rw single_eq_same,
+    exact h }
+end
+
+lemma support_single [decidable_eq B] :
+  function.support (pi.single a b) = if b = 0 then ∅ else {a} := by { split_ifs with h; simp [h] }
+
+lemma support_single_subset : function.support (pi.single a b) ⊆ {a} :=
+begin
+  classical,
+  rw support_single,
+  split_ifs;
+  simp
+end
+
+end pi