ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>self : HahnSeries Γ R<GOAL>(Function.support self.coeff).IsPWO
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<GOAL>Function.Injective HahnSeries.coeff
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>x y : HahnSeries Γ R<GOAL>x.coeff = y.coeff ↔ x = y
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>x : HahnSeries Γ R<GOAL>x.support.IsPWO
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>x : HahnSeries Γ R<GOAL>x.support.IsWF
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>x : HahnSeries Γ R<VAR>a : Γ<GOAL>a ∈ x.support ↔ x.coeff a ≠ 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>a : Γ<GOAL>HahnSeries.coeff 0 a = 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>x : HahnSeries Γ R<GOAL>x.coeff = 0 ↔ x = 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>x : HahnSeries Γ R<VAR>g : Γ<VAR>h : x.coeff g ≠ 0<GOAL>x ≠ 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<GOAL>HahnSeries.support 0 = ∅
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>x : HahnSeries Γ R<GOAL>x.support.Nonempty ↔ x ≠ 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>x : HahnSeries Γ R<GOAL>x.support = ∅ ↔ x = 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>f : Γ → R<VAR>h : (Function.support f).IsPWO<GOAL>{ coeff := f, isPWO_support' := h } = 0 ↔ f = 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>Γ' : Type u_3<VAR>PartialOrder Γ'<VAR>x : HahnSeries (Lex (Γ × Γ')) R<GOAL>HahnSeries.iterateEquiv.symm x = x.toIterate
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>Γ' : Type u_3<VAR>PartialOrder Γ'<VAR>x : HahnSeries Γ (HahnSeries Γ' R)<GOAL>HahnSeries.iterateEquiv x = x.ofIterate
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>a : Γ<VAR>r : R<GOAL>((HahnSeries.single a) r).coeff a = r
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>a b : Γ<VAR>r : R<VAR>h : b ≠ a<GOAL>((HahnSeries.single a) r).coeff b = 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>a b : Γ<VAR>r : R<GOAL>((HahnSeries.single a) r).coeff b = if b = a then r else 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>a : Γ<VAR>r : R<VAR>h : r ≠ 0<GOAL>((HahnSeries.single a) r).support = {a}
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>a : Γ<VAR>r : R<GOAL>((HahnSeries.single a) r).support ⊆ {a}
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>a : Γ<VAR>r : R<VAR>b : Γ<VAR>h : b ∈ ((HahnSeries.single a) r).support<GOAL>b = a
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>a : Γ<GOAL>(HahnSeries.single a) 0 = 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>a : Γ<GOAL>Function.Injective ⇑(HahnSeries.single a)
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>a : Γ<VAR>r : R<VAR>h : r ≠ 0<GOAL>(HahnSeries.single a) r ≠ 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>a : Γ<VAR>r : R<GOAL>(HahnSeries.single a) r = 0 ↔ r = 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<GOAL>HahnSeries.orderTop 0 = ⊤
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>x : HahnSeries Γ R<VAR>hx : x ≠ 0<GOAL>x.orderTop = ↑(⋯.min ⋯)
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>x : HahnSeries Γ R<GOAL>x ≠ 0 ↔ x.orderTop ≠ ⊤
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>x : HahnSeries Γ R<GOAL>x.orderTop = ⊤ ↔ x = 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>x : HahnSeries Γ R<VAR>hx : x ≠ 0<GOAL>x.orderTop.untop ⋯ = ⋯.min ⋯
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>x : HahnSeries Γ R<VAR>g : Γ<VAR>hg : x.orderTop = ↑g<GOAL>x.coeff g ≠ 0
<VAR>R : Type u_2<VAR>Zero R<VAR>Γ : Type u_3<VAR>LinearOrder Γ<VAR>x : HahnSeries Γ R<VAR>g : Γ<VAR>h : x.coeff g ≠ 0<GOAL>x.orderTop ≤ ↑g
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>a : Γ<VAR>r : R<VAR>h : r ≠ 0<GOAL>((HahnSeries.single a) r).orderTop = ↑a
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>a : Γ<VAR>r : R<GOAL>↑a ≤ ((HahnSeries.single a) r).orderTop
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>r : R<VAR>g g' : Γ<VAR>hgg' : g < g'<GOAL>↑g < ((HahnSeries.single g') r).orderTop
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>x : HahnSeries Γ R<VAR>i : Γ<VAR>hi : ↑i < x.orderTop<GOAL>x.coeff i = 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<GOAL>HahnSeries.leadingCoeff 0 = 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>x : HahnSeries Γ R<VAR>hx : x ≠ 0<GOAL>x.leadingCoeff = x.coeff (⋯.min ⋯)
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>x : HahnSeries Γ R<GOAL>x.leadingCoeff = 0 ↔ x = 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>x : HahnSeries Γ R<GOAL>x.leadingCoeff ≠ 0 ↔ x ≠ 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>a : Γ<VAR>r : R<GOAL>((HahnSeries.single a) r).leadingCoeff = r
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>Zero Γ<GOAL>HahnSeries.order 0 = 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>Zero Γ<VAR>x : HahnSeries Γ R<VAR>hx : x ≠ 0<GOAL>x.order = ⋯.min ⋯
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>Zero Γ<VAR>x : HahnSeries Γ R<VAR>hx : x ≠ 0<GOAL>↑x.order = x.orderTop
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>Zero Γ<VAR>x : HahnSeries Γ R<VAR>hx : x ≠ 0<GOAL>x.coeff x.order ≠ 0
<VAR>R : Type u_2<VAR>Zero R<VAR>Γ : Type u_3<VAR>LinearOrderedCancelAddCommMonoid Γ<VAR>x : HahnSeries Γ R<VAR>g : Γ<VAR>h : x.coeff g ≠ 0<GOAL>x.order ≤ g
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>a : Γ<VAR>r : R<VAR>Zero Γ<VAR>h : r ≠ 0<GOAL>((HahnSeries.single a) r).order = a
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>Zero Γ<VAR>x : HahnSeries Γ R<VAR>i : Γ<VAR>hi : i < x.order<GOAL>x.coeff i = 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>Zero Γ<VAR>x : HahnSeries Γ R<VAR>hx : x ≠ 0<GOAL>0 < x.orderTop ↔ 0 < x.order
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>Zero Γ<VAR>x : HahnSeries Γ R<VAR>hx : 0 < x.order<GOAL>0 < x.orderTop
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>Zero Γ<VAR>x : HahnSeries Γ R<GOAL>0 ≤ x.orderTop ↔ 0 ≤ x.order
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>Zero Γ<VAR>x : HahnSeries Γ R<GOAL>x.leadingCoeff = x.coeff x.order
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>Γ' : Type u_3<VAR>PartialOrder Γ'<VAR>f : Γ ↪o Γ'<VAR>x : HahnSeries Γ R<VAR>a : Γ<GOAL>(HahnSeries.embDomain f x).coeff (f a) = x.coeff a
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>Γ' : Type u_3<VAR>PartialOrder Γ'<VAR>f : Γ → Γ'<VAR>hfi : Function.Injective f<VAR>hf : ∀ (g g' : Γ), f g ≤ f g' ↔ g ≤ g'<VAR>x : HahnSeries Γ R<VAR>a : Γ<GOAL>(HahnSeries.embDomain { toFun := f, inj' := hfi, map_rel_iff' := ⋯ } x).coeff (f a) = x.coeff a
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>Γ' : Type u_3<VAR>PartialOrder Γ'<VAR>f : Γ ↪o Γ'<VAR>x : HahnSeries Γ R<VAR>b : Γ'<VAR>hb : b ∉ ⇑f '' x.support<GOAL>(HahnSeries.embDomain f x).coeff b = 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>Γ' : Type u_3<VAR>PartialOrder Γ'<VAR>f : Γ ↪o Γ'<VAR>x : HahnSeries Γ R<GOAL>(HahnSeries.embDomain f x).support ⊆ ⇑f '' x.support
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>Γ' : Type u_3<VAR>PartialOrder Γ'<VAR>f : Γ ↪o Γ'<VAR>x : HahnSeries Γ R<VAR>b : Γ'<VAR>hb : b ∉ Set.range ⇑f<GOAL>(HahnSeries.embDomain f x).coeff b = 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>Γ' : Type u_3<VAR>PartialOrder Γ'<VAR>f : Γ ↪o Γ'<GOAL>HahnSeries.embDomain f 0 = 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>Γ' : Type u_3<VAR>PartialOrder Γ'<VAR>f : Γ ↪o Γ'<VAR>g : Γ<VAR>r : R<GOAL>HahnSeries.embDomain f ((HahnSeries.single g) r) = (HahnSeries.single (f g)) r
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Zero R<VAR>Γ' : Type u_3<VAR>PartialOrder Γ'<VAR>f : Γ ↪o Γ'<GOAL>Function.Injective (HahnSeries.embDomain f)
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>Zero R<VAR>LinearOrder Γ<VAR>LocallyFiniteOrder Γ<VAR>f : Γ → R<VAR>hf : BddBelow (Function.support f)<GOAL>(Function.support f).IsPWO
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>Zero R<VAR>LinearOrder Γ<VAR>f : Γ → R<VAR>n : Γ<VAR>hn : ∀ m < n, f m = 0<GOAL>BddBelow (Function.support f)
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>Zero R<VAR>LinearOrder Γ<VAR>LocallyFiniteOrder Γ<VAR>f : Γ → R<VAR>hf : BddBelow (Function.support f)<GOAL>∀ (a : Γ), (HahnSeries.ofSuppBddBelow f hf).coeff a = f a
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>Zero R<VAR>LinearOrder Γ<VAR>Nonempty Γ<GOAL>BddBelow (Function.support 0)
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>Zero R<VAR>LinearOrder Γ<VAR>LocallyFiniteOrder Γ<VAR>Nonempty Γ<GOAL>HahnSeries.ofSuppBddBelow 0 ⋯ = 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>Zero R<VAR>LinearOrder Γ<VAR>LocallyFiniteOrder Γ<VAR>Zero Γ<VAR>f : Γ → R<VAR>hf : f ≠ 0<VAR>n : Γ<VAR>hn : ∀ m < n, f m = 0<GOAL>n ≤ (HahnSeries.ofSuppBddBelow f ⋯).order
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsNoetherianRing R<VAR>LocalRing R<VAR>IsDomain R<VAR>h' : Submodule.IsPrincipal (LocalRing.maximalIdeal R)<VAR>I : Ideal R<VAR>hI : I ≠ ⊥<GOAL>∃ n, I = LocalRing.maximalIdeal R ^ n
<VAR>R : Type u_1<VAR>CommRing R<VAR>LocalRing R<VAR>IsDomain R<VAR>IsDedekindDomain R<GOAL>Submodule.IsPrincipal (LocalRing.maximalIdeal R)
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsNoetherianRing R<VAR>LocalRing R<VAR>IsDomain R<GOAL>[IsPrincipalIdealRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = LocalRing.maximalIdeal R, Submodule.IsPrincipal (LocalRing.maximalIdeal R), FiniteDimensional.finrank (LocalRing.ResidueField R) (LocalRing.CotangentSpace R) ≤ 1, ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = LocalRing.maximalIdeal R ^ n].TFAE
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsNoetherianRing R<VAR>LocalRing R<VAR>IsDomain R<VAR>h : ¬IsField R<GOAL>[DiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime, Submodule.IsPrincipal (LocalRing.maximalIdeal R), FiniteDimensional.finrank (LocalRing.ResidueField R) (LocalRing.CotangentSpace R) = 1, ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = LocalRing.maximalIdeal R ^ n].TFAE
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsNoetherianRing R<VAR>LocalRing R<VAR>IsDomain R<GOAL>FiniteDimensional.finrank (LocalRing.ResidueField R) (LocalRing.CotangentSpace R) = 1 ↔ DiscreteValuationRing R
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>DiscreteValuationRing R<GOAL>FiniteDimensional.finrank (LocalRing.ResidueField R) (LocalRing.CotangentSpace R) = 1
<VAR>R : Type u_2<VAR>Semiring R<VAR>f : HahnSeries ℕ R<GOAL>HahnSeries.toPowerSeries f = PowerSeries.mk f.coeff
<VAR>R : Type u_2<VAR>Semiring R<VAR>f : PowerSeries R<VAR>n : ℕ<GOAL>(HahnSeries.toPowerSeries.symm f).coeff n = (PowerSeries.coeff R n) f
<VAR>R : Type u_2<VAR>Semiring R<VAR>f : HahnSeries ℕ R<VAR>n : ℕ<GOAL>(PowerSeries.coeff R n) (HahnSeries.toPowerSeries f) = f.coeff n
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>StrictOrderedSemiring Γ<GOAL>Function.Injective ⇑(HahnSeries.ofPowerSeries Γ R)
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>StrictOrderedSemiring Γ<VAR>x : PowerSeries R<GOAL>(HahnSeries.ofPowerSeries Γ R) x = HahnSeries.embDomain { toFun := Nat.cast, inj' := ⋯, map_rel_iff' := ⋯ } (HahnSeries.toPowerSeries.symm x)
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>StrictOrderedSemiring Γ<VAR>x : PowerSeries R<VAR>n : ℕ<GOAL>((HahnSeries.ofPowerSeries Γ R) x).coeff ↑n = (PowerSeries.coeff R n) x
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>StrictOrderedSemiring Γ<VAR>r : R<GOAL>(HahnSeries.ofPowerSeries Γ R) ((PowerSeries.C R) r) = HahnSeries.C r
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>StrictOrderedSemiring Γ<GOAL>(HahnSeries.ofPowerSeries Γ R) PowerSeries.X = (HahnSeries.single 1) 1
<VAR>Γ : Type u_1<VAR>StrictOrderedSemiring Γ<VAR>R : Type u_3<VAR>Semiring R<VAR>n : ℕ<GOAL>(HahnSeries.ofPowerSeries Γ R) (PowerSeries.X ^ n) = (HahnSeries.single ↑n) 1
<VAR>R : Type u_2<VAR>Semiring R<VAR>σ : Type u_3<VAR>Finite σ<VAR>f : HahnSeries (σ →₀ ℕ) R<GOAL>∀ (a : σ →₀ ℕ), HahnSeries.toMvPowerSeries f a = f.coeff a
<VAR>R : Type u_2<VAR>Semiring R<VAR>σ : Type u_3<VAR>Finite σ<VAR>f : MvPowerSeries σ R<GOAL>(HahnSeries.toMvPowerSeries.symm f).coeff = f
<VAR>R : Type u_2<VAR>Semiring R<VAR>σ : Type u_3<VAR>Finite σ<VAR>f : HahnSeries (σ →₀ ℕ) R<VAR>n : σ →₀ ℕ<GOAL>(MvPowerSeries.coeff R n) (HahnSeries.toMvPowerSeries f) = f.coeff n
<VAR>R : Type u_2<VAR>Semiring R<VAR>σ : Type u_3<VAR>Finite σ<VAR>f : MvPowerSeries σ R<VAR>n : σ →₀ ℕ<GOAL>(HahnSeries.toMvPowerSeries.symm f).coeff n = (MvPowerSeries.coeff R n) f
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>A : Type u_3<VAR>Semiring A<VAR>Algebra R A<VAR>f : PowerSeries A<VAR>n : ℕ<GOAL>((HahnSeries.toPowerSeriesAlg R).symm f).coeff n = (PowerSeries.coeff A n) f
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>A : Type u_3<VAR>Semiring A<VAR>Algebra R A<VAR>f : HahnSeries ℕ A<GOAL>(HahnSeries.toPowerSeriesAlg R) f = PowerSeries.mk f.coeff
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>A : Type u_3<VAR>Semiring A<VAR>Algebra R A<VAR>StrictOrderedSemiring Γ<GOAL>∀ (a : PowerSeries A) (b : Γ), ((HahnSeries.ofPowerSeriesAlg Γ R) a).coeff b = if h : ∃ x, ¬(PowerSeries.coeff A x) a = 0 ∧ ↑x = b then (PowerSeries.coeff A (Classical.choose ⋯)) a else 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>StrictOrderedSemiring Γ<VAR>S : Type u_4<VAR>CommSemiring S<VAR>Algebra S (PowerSeries R)<VAR>x : S<GOAL>(algebraMap S (HahnSeries Γ R)) x = (HahnSeries.ofPowerSeries Γ R) ((algebraMap S (PowerSeries R)) x)
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>StrictOrderedSemiring Γ<VAR>f : R[X]<GOAL>(algebraMap R[X] (HahnSeries Γ R)) f = (HahnSeries.ofPowerSeries Γ R) ↑f
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>StrictOrderedSemiring Γ<GOAL>Function.Injective ⇑(algebraMap R[X] (HahnSeries Γ R))
<VAR>R : Type u<VAR>CommRing R<GOAL>IsBezout R ↔ ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>IsBezout R<GOAL>IsBezout S
<VAR>R : Type u<VAR>CommRing R<VAR>IsBezout R<VAR>IsDomain R<GOAL>[IsNoetherianRing R, IsPrincipalIdealRing R, UniqueFactorizationMonoid R, WfDvdMonoid R].TFAE
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : RingHom.RespectsIso P<VAR>R S T : CommRingCat<VAR>f : R ⟶ S<VAR>g : S ⟶ T<VAR>CategoryTheory.IsIso f<GOAL>P (f ≫ g) ↔ P g
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : RingHom.RespectsIso P<VAR>R S T : CommRingCat<VAR>f : R ⟶ S<VAR>g : S ⟶ T<VAR>CategoryTheory.IsIso g<GOAL>P (f ≫ g) ↔ P f
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : RingHom.RespectsIso P<VAR>R S : Type u<VAR>R' S' : Type u<VAR>CommRing R<VAR>CommRing S<VAR>CommRing R'<VAR>CommRing S'<VAR>Algebra R R'<VAR>Algebra S S'<VAR>f : R →+* S<VAR>r : R<VAR>IsLocalization.Away r R'<VAR>IsLocalization.Away (f r) S'<GOAL>P (Localization.awayMap f r) ↔ P (IsLocalization.Away.map R' S' f r)
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : RingHom.StableUnderComposition P<VAR>hP' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), P e.toRingHom<GOAL>RingHom.RespectsIso P
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>h₁ : RingHom.RespectsIso P<VAR>h₂ : ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S] [inst_4 : Algebra R T], P (algebraMap R T) → P Algebra.TensorProduct.includeLeftRingHom<GOAL>RingHom.StableUnderBaseChange P
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : RingHom.StableUnderBaseChange P<VAR>hP' : RingHom.RespectsIso P<VAR>R S T : CommRingCat<VAR>f : R ⟶ S<VAR>g : R ⟶ T<VAR>H : P g<GOAL>P (CategoryTheory.Limits.pushout.inl f g)
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<GOAL>(RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) ↔ (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => P).RespectsIso
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddMonoid R<VAR>x y : HahnSeries Γ R<GOAL>(x + y).coeff = x.coeff + y.coeff
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddMonoid R<VAR>x y : HahnSeries Γ R<VAR>a : Γ<GOAL>(x + y).coeff a = x.coeff a + y.coeff a
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddMonoid R<VAR>x : (HahnSeries Γ R)ᵃᵒᵖ<VAR>a : Γ<GOAL>(HahnSeries.addOppositeEquiv.symm x).coeff a = AddOpposite.op ((AddOpposite.unop x).coeff a)
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddMonoid R<VAR>x : HahnSeries Γ Rᵃᵒᵖ<GOAL>HahnSeries.addOppositeEquiv x = AddOpposite.op { coeff := fun a => AddOpposite.unop (x.coeff a), isPWO_support' := ⋯ }
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddMonoid R<VAR>x : HahnSeries Γ Rᵃᵒᵖ<GOAL>(AddOpposite.unop (HahnSeries.addOppositeEquiv x)).support = x.support
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddMonoid R<VAR>x : (HahnSeries Γ R)ᵃᵒᵖ<GOAL>(HahnSeries.addOppositeEquiv.symm x).support = (AddOpposite.unop x).support
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddMonoid R<VAR>x : HahnSeries Γ Rᵃᵒᵖ<GOAL>(AddOpposite.unop (HahnSeries.addOppositeEquiv x)).orderTop = x.orderTop
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddMonoid R<VAR>x : (HahnSeries Γ R)ᵃᵒᵖ<GOAL>(HahnSeries.addOppositeEquiv.symm x).orderTop = (AddOpposite.unop x).orderTop
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddMonoid R<VAR>x : HahnSeries Γ Rᵃᵒᵖ<GOAL>(AddOpposite.unop (HahnSeries.addOppositeEquiv x)).leadingCoeff = AddOpposite.unop x.leadingCoeff
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddMonoid R<VAR>x : (HahnSeries Γ R)ᵃᵒᵖ<GOAL>(HahnSeries.addOppositeEquiv.symm x).leadingCoeff = AddOpposite.op (AddOpposite.unop x).leadingCoeff
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddMonoid R<VAR>x y : HahnSeries Γ R<GOAL>(x + y).support ⊆ x.support ∪ y.support
<VAR>R : Type u_2<VAR>AddMonoid R<VAR>Γ : Type u_3<VAR>LinearOrder Γ<VAR>x y : HahnSeries Γ R<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hxy : x + y ≠ 0<GOAL>min (⋯.min ⋯) (⋯.min ⋯) ≤ ⋯.min ⋯
<VAR>R : Type u_2<VAR>AddMonoid R<VAR>Γ : Type u_3<VAR>LinearOrder Γ<VAR>x y : HahnSeries Γ R<GOAL>min x.orderTop y.orderTop ≤ (x + y).orderTop
<VAR>R : Type u_2<VAR>AddMonoid R<VAR>Γ : Type u_3<VAR>Zero Γ<VAR>LinearOrder Γ<VAR>x y : HahnSeries Γ R<VAR>hxy : x + y ≠ 0<GOAL>min x.order y.order ≤ (x + y).order
<VAR>R : Type u_2<VAR>AddMonoid R<VAR>Γ : Type u_3<VAR>LinearOrder Γ<VAR>x y : HahnSeries Γ R<VAR>hxy : x.orderTop < y.orderTop<GOAL>(x + y).orderTop = x.orderTop
<VAR>R : Type u_2<VAR>AddMonoid R<VAR>Γ : Type u_3<VAR>LinearOrder Γ<VAR>x y : HahnSeries Γ R<VAR>hxy : y.orderTop < x.orderTop<GOAL>(x + y).orderTop = y.orderTop
<VAR>R : Type u_2<VAR>AddMonoid R<VAR>Γ : Type u_3<VAR>LinearOrder Γ<VAR>x y : HahnSeries Γ R<VAR>hxy : x.orderTop < y.orderTop<GOAL>(x + y).leadingCoeff = x.leadingCoeff
<VAR>R : Type u_2<VAR>AddMonoid R<VAR>Γ : Type u_3<VAR>LinearOrder Γ<VAR>x y : HahnSeries Γ R<VAR>hxy : y.orderTop < x.orderTop<GOAL>(x + y).leadingCoeff = y.leadingCoeff
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddMonoid R<VAR>a : Γ<VAR>r : R<VAR>j : Γ<GOAL>((HahnSeries.single.addMonoidHom a) r).coeff j = Pi.single a r j
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddMonoid R<VAR>g : Γ<VAR>f : HahnSeries Γ R<GOAL>(HahnSeries.coeff.addMonoidHom g) f = f.coeff g
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddMonoid R<VAR>Γ' : Type u_3<VAR>PartialOrder Γ'<VAR>f : Γ ↪o Γ'<VAR>x y : HahnSeries Γ R<GOAL>HahnSeries.embDomain f (x + y) = HahnSeries.embDomain f x + HahnSeries.embDomain f y
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddGroup R<VAR>x : HahnSeries Γ R<GOAL>(-x).coeff = -x.coeff
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddGroup R<VAR>x : HahnSeries Γ R<VAR>a : Γ<GOAL>(-x).coeff a = -x.coeff a
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddGroup R<VAR>x : HahnSeries Γ R<GOAL>(-x).support = x.support
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddGroup R<VAR>x y : HahnSeries Γ R<GOAL>(x - y).coeff = x.coeff - y.coeff
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddGroup R<VAR>x y : HahnSeries Γ R<VAR>a : Γ<GOAL>(x - y).coeff a = x.coeff a - y.coeff a
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddGroup R<VAR>x : HahnSeries Γ R<GOAL>(-x).orderTop = x.orderTop
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddGroup R<VAR>Zero Γ<VAR>f : HahnSeries Γ R<GOAL>(-f).order = f.order
<VAR>R : Type u_2<VAR>AddGroup R<VAR>Γ : Type u_3<VAR>LinearOrder Γ<VAR>x y : HahnSeries Γ R<GOAL>min x.orderTop y.orderTop ≤ (x - y).orderTop
<VAR>R : Type u_2<VAR>AddGroup R<VAR>Γ : Type u_3<VAR>LinearOrder Γ<VAR>x y : HahnSeries Γ R<VAR>hxy : x.orderTop < y.orderTop<GOAL>(x - y).orderTop = x.orderTop
<VAR>R : Type u_2<VAR>AddGroup R<VAR>Γ : Type u_3<VAR>LinearOrder Γ<VAR>x y : HahnSeries Γ R<VAR>hxy : x.orderTop < y.orderTop<GOAL>(x - y).leadingCoeff = x.leadingCoeff
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>V : Type u_3<VAR>Zero V<VAR>SMulZeroClass R V<VAR>r : R<VAR>x : HahnSeries Γ V<VAR>a : Γ<GOAL>(r • x).coeff a = r • x.coeff a
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>V : Type u_3<VAR>Zero V<VAR>SMulZeroClass R V<VAR>r : R<VAR>x : HahnSeries Γ V<GOAL>¬(r • x).orderTop < x.orderTop
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>V : Type u_3<VAR>Zero V<VAR>SMulZeroClass R V<VAR>Zero Γ<VAR>r : R<VAR>x : HahnSeries Γ V<VAR>h : r • x ≠ 0<GOAL>¬(r • x).order < x.order
<VAR>R : Type u_2<VAR>V : Type u_3<VAR>Zero V<VAR>SMulZeroClass R V<VAR>Γ : Type u_4<VAR>Zero Γ<VAR>LinearOrder Γ<VAR>r : R<VAR>x : HahnSeries Γ V<VAR>h : r • x ≠ 0<GOAL>x.order ≤ (r • x).order
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Semiring R<VAR>V : Type u_3<VAR>AddCommMonoid V<VAR>Module R V<VAR>a : Γ<GOAL>∀ (a_1 : V), (HahnSeries.single.linearMap a) a_1 = (↑(HahnSeries.single.addMonoidHom a)).toFun a_1
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Semiring R<VAR>V : Type u_3<VAR>AddCommMonoid V<VAR>Module R V<VAR>g : Γ<GOAL>∀ (a : HahnSeries Γ V), (HahnSeries.coeff.linearMap g) a = (↑(HahnSeries.coeff.addMonoidHom g)).toFun a
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Semiring R<VAR>Γ' : Type u_4<VAR>PartialOrder Γ'<VAR>f : Γ ↪o Γ'<VAR>r : R<VAR>x : HahnSeries Γ R<GOAL>HahnSeries.embDomain f (r • x) = r • HahnSeries.embDomain f x
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>Semiring R<VAR>Γ' : Type u_4<VAR>PartialOrder Γ'<VAR>f : Γ ↪o Γ'<GOAL>∀ (a : HahnSeries Γ R), (HahnSeries.embDomainLinearMap f) a = HahnSeries.embDomain f a
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>a : S<GOAL>1 ⊗ₜ[R] a - a ⊗ₜ[R] 1 ∈ KaehlerDifferential.ideal R S
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>M : Type u_1<VAR>AddCommGroup M<VAR>Module R M<VAR>Module S M<VAR>IsScalarTower R S M<VAR>D : Derivation R S M<VAR>s t : S<GOAL>D.tensorProductTo (s ⊗ₜ[R] t) = s • D t
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>M : Type u_1<VAR>AddCommGroup M<VAR>Module R M<VAR>Module S M<VAR>IsScalarTower R S M<VAR>D : Derivation R S M<VAR>x y : TensorProduct R S S<GOAL>D.tensorProductTo (x * y) = (Algebra.TensorProduct.lmul' R) x • D.tensorProductTo y + (Algebra.TensorProduct.lmul' R) y • D.tensorProductTo x