Commit 2024-05-17 08:20 a53131f8

View on Github →

feat: HahnSeries on Lex product (#10781) This PR implements an equivalence between HahnSeries Γ (HahnSeries Γ' R) and HahnSeries (Γ ×ₗ Γ') R. We do this by showing that a subset of the lexicographic product is partially well-ordered if and only if its projection to the first coordinate is partially well-ordered and its intersection with each fiber is partially well-ordered.

Estimated changes

Modified Mathlib/Algebra/Function/Support.lean

added theorem Function.mulSupport_curry'

added theorem Function.mulSupport_curry

Modified Mathlib/Data/Prod/Lex.lean

added theorem Prod.Lex.monotone_fst

Modified Mathlib/Order/WellFoundedSet.lean

added theorem Set.PartiallyWellOrderedOn.ProdLex_iff

added theorem Set.PartiallyWellOrderedOn.fiberProdLex

added theorem Set.PartiallyWellOrderedOn.imageProdLex

added theorem Set.PartiallyWellOrderedOn.subsetProdLex

Modified Mathlib/RingTheory/HahnSeries/Basic.lean

added def HahnSeries.iterateEquiv

added theorem HahnSeries.mk_eq_zero

added def HahnSeries.ofIterate

added def HahnSeries.toIterate

deleted def HahnSeries.to_iterate