Formal power series - Inverses

If the constant coefficient of a formal (univariate) power series is invertible, then this formal power series is invertible. (See the discussion in Mathlib.RingTheory.MvPowerSeries.Inverse for the construction.)

Formal (univariate) power series over a local ring form a local ring.

def PowerSeries.inv.aux {R : Type u_1} [Ring R] : R → PowerSeries R → PowerSeries R

Auxiliary function used for computing inverse of a power series

Equations

• PowerSeries.inv.aux = MvPowerSeries.inv.aux

theorem PowerSeries.coeff_inv_aux {R : Type u_1} [Ring R] (n : ℕ) (a : R) (φ : PowerSeries R) : (PowerSeries.coeff R n) (PowerSeries.inv.aux a φ) = if n = 0 then a else -a * Finset.sum (Finset.antidiagonal n) fun (x : ℕ × ℕ) => if x.2 < n then (PowerSeries.coeff R x.1) φ * (PowerSeries.coeff R x.2) (PowerSeries.inv.aux a φ) else 0

def PowerSeries.invOfUnit {R : Type u_1} [Ring R] (φ : PowerSeries R) (u : Rˣ) : PowerSeries R

A formal power series is invertible if the constant coefficient is invertible.

Equations

• PowerSeries.invOfUnit φ u = MvPowerSeries.invOfUnit φ u

theorem PowerSeries.coeff_invOfUnit {R : Type u_1} [Ring R] (n : ℕ) (φ : PowerSeries R) (u : Rˣ) : (PowerSeries.coeff R n) (PowerSeries.invOfUnit φ u) = if n = 0 then ↑u⁻¹ else -↑u⁻¹ * Finset.sum (Finset.antidiagonal n) fun (x : ℕ × ℕ) => if x.2 < n then (PowerSeries.coeff R x.1) φ * (PowerSeries.coeff R x.2) (PowerSeries.invOfUnit φ u) else 0

@[simp]

theorem PowerSeries.constantCoeff_invOfUnit {R : Type u_1} [Ring R] (φ : PowerSeries R) (u : Rˣ) : (PowerSeries.constantCoeff R) (PowerSeries.invOfUnit φ u) = ↑u⁻¹

theorem PowerSeries.mul_invOfUnit {R : Type u_1} [Ring R] (φ : PowerSeries R) (u : Rˣ) (h : (PowerSeries.constantCoeff R) φ = ↑u) : φ * PowerSeries.invOfUnit φ u = 1

theorem PowerSeries.sub_const_eq_shift_mul_X {R : Type u_1} [Ring R] (φ : PowerSeries R) : φ - (PowerSeries.C R) ((PowerSeries.constantCoeff R) φ) = (PowerSeries.mk fun (p : ℕ) => (PowerSeries.coeff R (p + 1)) φ) * PowerSeries.X

Two ways of removing the constant coefficient of a power series are the same.

theorem PowerSeries.sub_const_eq_X_mul_shift {R : Type u_1} [Ring R] (φ : PowerSeries R) : φ - (PowerSeries.C R) ((PowerSeries.constantCoeff R) φ) = PowerSeries.X * PowerSeries.mk fun (p : ℕ) => (PowerSeries.coeff R (p + 1)) φ

def PowerSeries.inv {k : Type u_2} [Field k] : PowerSeries k → PowerSeries k

The inverse 1/f of a power series f defined over a field

Equations

• PowerSeries.inv = MvPowerSeries.inv

instance PowerSeries.instInvPowerSeries {k : Type u_2} [Field k] : Inv (PowerSeries k)

Equations

• PowerSeries.instInvPowerSeries = { inv := PowerSeries.inv }

theorem PowerSeries.inv_eq_inv_aux {k : Type u_2} [Field k] (φ : PowerSeries k) : φ⁻¹ = PowerSeries.inv.aux ((PowerSeries.constantCoeff k) φ)⁻¹ φ

theorem PowerSeries.coeff_inv {k : Type u_2} [Field k] (n : ℕ) (φ : PowerSeries k) : (PowerSeries.coeff k n) φ⁻¹ = if n = 0 then ((PowerSeries.constantCoeff k) φ)⁻¹ else -((PowerSeries.constantCoeff k) φ)⁻¹ * Finset.sum (Finset.antidiagonal n) fun (x : ℕ × ℕ) => if x.2 < n then (PowerSeries.coeff k x.1) φ * (PowerSeries.coeff k x.2) φ⁻¹ else 0

@[simp]

theorem PowerSeries.constantCoeff_inv {k : Type u_2} [Field k] (φ : PowerSeries k) : (PowerSeries.constantCoeff k) φ⁻¹ = ((PowerSeries.constantCoeff k) φ)⁻¹

theorem PowerSeries.inv_eq_zero {k : Type u_2} [Field k] {φ : PowerSeries k} : φ⁻¹ = 0 ↔ (PowerSeries.constantCoeff k) φ = 0

@[simp]

theorem PowerSeries.zero_inv {k : Type u_2} [Field k] : 0⁻¹ = 0

theorem PowerSeries.invOfUnit_eq {k : Type u_2} [Field k] (φ : PowerSeries k) (h : (PowerSeries.constantCoeff k) φ ≠ 0) : PowerSeries.invOfUnit φ (Units.mk0 ((PowerSeries.constantCoeff k) φ) h) = φ⁻¹

@[simp]

theorem PowerSeries.invOfUnit_eq' {k : Type u_2} [Field k] (φ : PowerSeries k) (u : kˣ) (h : (PowerSeries.constantCoeff k) φ = ↑u) : PowerSeries.invOfUnit φ u = φ⁻¹

@[simp]

theorem PowerSeries.mul_inv_cancel {k : Type u_2} [Field k] (φ : PowerSeries k) (h : (PowerSeries.constantCoeff k) φ ≠ 0) : φ * φ⁻¹ = 1

@[simp]

theorem PowerSeries.inv_mul_cancel {k : Type u_2} [Field k] (φ : PowerSeries k) (h : (PowerSeries.constantCoeff k) φ ≠ 0) : φ⁻¹ * φ = 1

theorem PowerSeries.eq_mul_inv_iff_mul_eq {k : Type u_2} [Field k] {φ₁ : PowerSeries k} {φ₂ : PowerSeries k} {φ₃ : PowerSeries k} (h : (PowerSeries.constantCoeff k) φ₃ ≠ 0) : φ₁ = φ₂ * φ₃⁻¹ ↔ φ₁ * φ₃ = φ₂

theorem PowerSeries.eq_inv_iff_mul_eq_one {k : Type u_2} [Field k] {φ : PowerSeries k} {ψ : PowerSeries k} (h : (PowerSeries.constantCoeff k) ψ ≠ 0) : φ = ψ⁻¹ ↔ φ * ψ = 1

theorem PowerSeries.inv_eq_iff_mul_eq_one {k : Type u_2} [Field k] {φ : PowerSeries k} {ψ : PowerSeries k} (h : (PowerSeries.constantCoeff k) ψ ≠ 0) : ψ⁻¹ = φ ↔ φ * ψ = 1

@[simp]

theorem PowerSeries.mul_inv_rev {k : Type u_2} [Field k] (φ : PowerSeries k) (ψ : PowerSeries k) : (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹

instance PowerSeries.instInvOneClassPowerSeries {k : Type u_2} [Field k] : InvOneClass (PowerSeries k)

Equations

• PowerSeries.instInvOneClassPowerSeries = let __src := inferInstanceAs (InvOneClass (MvPowerSeries Unit k)); InvOneClass.mk ⋯

@[simp]

theorem PowerSeries.C_inv {k : Type u_2} [Field k] (r : k) : ((PowerSeries.C k) r)⁻¹ = (PowerSeries.C k) r⁻¹

@[simp]

theorem PowerSeries.X_inv {k : Type u_2} [Field k] : PowerSeries.X⁻¹ = 0

@[simp]

theorem PowerSeries.smul_inv {k : Type u_2} [Field k] (r : k) (φ : PowerSeries k) : (r • φ)⁻¹ = r⁻¹ • φ⁻¹

instance PowerSeries.map.isLocalRingHom {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) [IsLocalRingHom f] : IsLocalRingHom (PowerSeries.map f)

Equations

• ⋯ = ⋯

instance PowerSeries.instLocalRingPowerSeriesInstSemiringPowerSeriesToSemiringToCommSemiring {R : Type u_1} [CommRing R] [LocalRing R] : LocalRing (PowerSeries R)

Equations

• ⋯ = ⋯