feat(ring_theory/hahn_series): algebra structure, equivalences with p…

…ower series (#6540)

Places an `algebra` structure on `hahn_series`
Defines a `ring_equiv` and when relevant an `alg_equiv` between `hahn_series nat R` and `power_series R`.



Co-authored-by: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr>

src/data/polynomial/algebra_map.lean

@@ -44,6 +44,17 @@ lemma C_eq_algebra_map {R : Type*} [comm_ring R] (r : R) :
   C r = algebra_map R (polynomial R) r :=
 rfl
 
+instance [nontrivial A] : nontrivial (subalgebra R (polynomial A)) :=
+⟨⟨⊥, ⊤, begin
+  rw [ne.def, subalgebra.ext_iff, not_forall],
+  refine ⟨X, _⟩,
+  simp only [algebra.mem_bot, not_exists, set.mem_range, iff_true, algebra.mem_top,
+    algebra_map_apply, not_forall],
+  intro x,
+  rw [ext_iff, not_forall],
+  refine ⟨1, _⟩,
+  simp [coeff_C],
+end⟩⟩
 
 @[simp]
 lemma alg_hom_eval₂_algebra_map

src/order/well_founded_set.lean

@@ -66,6 +66,9 @@ variables [has_lt α]
 /-- `s.is_wf` indicates that `<` is well-founded when restricted to `s`. -/
 def is_wf (s : set α) : Prop := well_founded_on s (<)
 
+lemma is_wf_univ_iff : is_wf (univ : set α) ↔ well_founded ((<) : α → α → Prop) :=
+by simp [is_wf, well_founded_on_iff]
+
 variables {s t : set α}
 
 theorem is_wf.mono (h : is_wf t) (st : s ⊆ t) : is_wf s :=
@@ -453,3 +456,7 @@ theorem is_wf_support_mul_antidiagonal :
 (hs.mul ht).mono support_mul_antidiagonal_subset_mul
 
 end finset
+
+lemma well_founded.is_wf [has_lt α] (h : well_founded ((<) : α → α → Prop)) (s : set α) :
+  s.is_wf :=
+(set.is_wf_univ_iff.2 h).mono (set.subset_univ s)