def MvPowerSeries.equivCongrLeft (R : Type u_1) (σ : Type u_2) (τ : Type u_3) (e : σ ≃ τ) : MvPowerSeries σ R ≃ MvPowerSeries τ R

Equations

• MvPowerSeries.equivCongrLeft R σ τ e = (Finsupp.equivCongrLeft e).arrowCongr' (Equiv.refl R)

@[simp]

theorem MvPowerSeries.equivCongrLeft_apply (R : Type u_1) (σ : Type u_2) (τ : Type u_3) (e : σ ≃ τ) (f : (σ →₀ ℕ) → R) (a✝ : τ →₀ ℕ) : (equivCongrLeft R σ τ e) f a✝ = f (Finsupp.equivMapDomain e.symm a✝)

@[simp]

theorem MvPowerSeries.equivCongrLeft_symm_apply (R : Type u_1) (σ : Type u_2) (τ : Type u_3) (e : σ ≃ τ) (f : (τ →₀ ℕ) → R) (a✝ : σ →₀ ℕ) : (equivCongrLeft R σ τ e).symm f a✝ = f (Finsupp.equivMapDomain e a✝)

def MvPowerSeries.ringEquivCongrLeft (R : Type u_1) (σ : Type u_2) (τ : Type u_3) [CommRing R] (e : σ ≃ τ) : MvPowerSeries σ R ≃+* MvPowerSeries τ R

Equations

• MvPowerSeries.ringEquivCongrLeft R σ τ e = { toEquiv := MvPowerSeries.equivCongrLeft R σ τ e, map_mul' := ⋯, map_add' := ⋯ }

noncomputable def MvPowerSeries.equivSum (R : Type u_1) (σ : Type u_2) (τ : Type u_3) : MvPowerSeries (σ ⊕ τ) R ≃ MvPowerSeries σ (MvPowerSeries τ R)

Equations

• MvPowerSeries.equivSum R σ τ = id ((Finsupp.sumFinsuppEquivProdFinsupp.arrowCongr' (Equiv.refl R)).trans (Equiv.curry (σ →₀ ℕ) (τ →₀ ℕ) R))

@[simp]

theorem MvPowerSeries.equivSum_apply (R : Type u_1) (σ : Type u_2) (τ : Type u_3) (a✝ : (σ ⊕ τ →₀ ℕ) → R) (a✝¹ : σ →₀ ℕ) (a✝² : τ →₀ ℕ) : (equivSum R σ τ) a✝ a✝¹ a✝² = a✝ (a✝¹.sumElim a✝²)

@[simp]

theorem MvPowerSeries.equivSum_symm_apply (R : Type u_1) (σ : Type u_2) (τ : Type u_3) (a✝ : (σ →₀ ℕ) → (τ →₀ ℕ) → R) (a✝¹ : σ ⊕ τ →₀ ℕ) : (equivSum R σ τ).symm a✝ a✝¹ = a✝ (Finsupp.comapDomain Sum.inl a✝¹ ⋯) (Finsupp.comapDomain Sum.inr a✝¹ ⋯)

noncomputable def MvPowerSeries.auxequiv (σ : Type u_2) (τ : Type u_3) : (σ ⊕ τ →₀ ℕ) × (σ ⊕ τ →₀ ℕ) ≃ ((σ →₀ ℕ) × (σ →₀ ℕ)) × (τ →₀ ℕ) × (τ →₀ ℕ)

Equations

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

@[simp]

theorem MvPowerSeries.auxequiv_apply (σ : Type u_2) (τ : Type u_3) (a✝ : (σ ⊕ τ →₀ ℕ) × (σ ⊕ τ →₀ ℕ)) : (auxequiv σ τ) a✝ = ((Finsupp.comapDomain Sum.inl a✝.1 ⋯, Finsupp.comapDomain Sum.inl a✝.2 ⋯), Finsupp.comapDomain Sum.inr a✝.1 ⋯, Finsupp.comapDomain Sum.inr a✝.2 ⋯)

@[simp]

theorem MvPowerSeries.auxequiv_symm_apply (σ : Type u_2) (τ : Type u_3) (a✝ : ((σ →₀ ℕ) × (σ →₀ ℕ)) × (τ →₀ ℕ) × (τ →₀ ℕ)) : (auxequiv σ τ).symm a✝ = (a✝.1.1.sumElim a✝.2.1, a✝.1.2.sumElim a✝.2.2)

noncomputable def MvPowerSeries.ringEquivSum' (R : Type u_1) (σ : Type u_2) (τ : Type u_3) [CommRing R] : MvPowerSeries (σ ⊕ τ) R ≃+* MvPowerSeries σ (MvPowerSeries τ R)

Equations

• MvPowerSeries.ringEquivSum' R σ τ = { toEquiv := MvPowerSeries.equivSum R σ τ, map_mul' := ⋯, map_add' := ⋯ }

noncomputable def MvPowerSeries.subsingleton_equiv (R : Type u_1) (σ : Type u_2) [CommRing R] [IsEmpty σ] : MvPowerSeries σ R ≃+* R

Equations

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

instance MvPowerSeries.instIsNoetherianRingFin_schlessinger (R : Type u_1) [CommRing R] [IsNoetherianRing R] (r : ℕ) : IsNoetherianRing (MvPowerSeries (Fin r) R)

instance MvPowerSeries.instIsNoetherianRingOfFinite_schlessinger (R : Type u_1) (σ : Type u_2) [CommRing R] [IsNoetherianRing R] [Finite σ] : IsNoetherianRing (MvPowerSeries σ R)