Multiplication of normalized exponent-subgroup parts

LM24, Corollary 6.5.4 states that the normalized H-part of a product is the product of the normalized H-parts. Its proof uses a specific Ritt-factorisation consequence: a normalized H-divisor of a product of finite-support real series can be split into normalized H-divisors of the two factors.

This module names that prerequisite explicitly and proves the complete reduction from it. The prerequisite is neither installed as an instance nor folded into the definition of a normalized H-part. Thus the intrinsic definition and uniqueness theorem remain independent of the later Ritt and greatest-common-divisor proof.

def HahnSeries.Nonpositive.HasNormalizedHDivisorRefinement (H : AddSubgroup ℝ) {K : Type v} [Field K] : Prop

Every normalized finite-support H-divisor of a product of finite-support real series splits as a product of normalized H-divisors of the two factors. This is the exact factor-splitting input used in LM24's proof of Corollary 6.5.4.

Equations

• One or more equations did not get rendered due to their size.

theorem HahnSeries.Nonpositive.hasNormalizedHDivisorRefinement_iff (H : AddSubgroup ℝ) {K : Type v} [Field K] : HasNormalizedHDivisorRefinement H ↔ ∀ (p q : ↥FiniteSupportRing) (r : ConstantTermOneFiniteSupport), (finiteSupportToReal H) ↑r ∣ p * q → ∃ (r₁ : ConstantTermOneFiniteSupport) (r₂ : ConstantTermOneFiniteSupport), r = r₁ * r₂ ∧ (finiteSupportToReal H) ↑r₁ ∣ p ∧ (finiteSupportToReal H) ↑r₂ ∣ q

Characterization of normalized H-divisor refinement by factor witnesses.

theorem HahnSeries.Nonpositive.isNormalizedHPart_mul (H : AddSubgroup ℝ) {K : Type v} [Field K] (hrefine : HasNormalizedHDivisorRefinement H) {p q : ↥FiniteSupportRing} {pH qH : ConstantTermOneFiniteSupport} (hpH : IsNormalizedHPart H p pH) (hqH : IsNormalizedHPart H q qH) : IsNormalizedHPart H (p * q) (pH * qH)

The product of two normalized H-parts satisfies the normalized-part divisibility characterization for the product.

theorem HahnSeries.Nonpositive.normalizedHPart_mul_eq (H : AddSubgroup ℝ) {K : Type v} [Field K] (hrefine : HasNormalizedHDivisorRefinement H) {p q : ↥FiniteSupportRing} {pH qH pqH : ConstantTermOneFiniteSupport} (hpH : IsNormalizedHPart H p pH) (hqH : IsNormalizedHPart H q qH) (hpqH : IsNormalizedHPart H (p * q) pqH) : pqH = pH * qH

Relational form of LM24, Corollary 6.5.4: any normalized H-part of a product equals the product of normalized H-parts of its factors.