Documentation

Mathlib.RingTheory.PowerSeries.Inverse

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.

Formal (univariate) power series over a field form a discrete valuation ring, and a normalization monoid. The definition residueFieldOfPowerSeries provides the isomorphism between the residue field of k⟦X⟧ and k, when k is a field.

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

Auxiliary function used for computing inverse of a power series

Equations
  • PowerSeries.inv.aux = MvPowerSeries.inv.aux
Instances For
    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 * xFinset.antidiagonal n, 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ˣ) :

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

    Equations
    Instances For
      theorem PowerSeries.coeff_invOfUnit {R : Type u_1} [Ring R] (n : ) (φ : PowerSeries R) (u : Rˣ) :
      (PowerSeries.coeff R n) (φ.invOfUnit u) = if n = 0 then u⁻¹ else -u⁻¹ * xFinset.antidiagonal n, if x.2 < n then (PowerSeries.coeff R x.1) φ * (PowerSeries.coeff R x.2) (φ.invOfUnit u) else 0
      @[simp]
      theorem PowerSeries.constantCoeff_invOfUnit {R : Type u_1} [Ring R] (φ : PowerSeries R) (u : Rˣ) :
      (PowerSeries.constantCoeff R) (φ.invOfUnit u) = u⁻¹
      @[simp]
      theorem PowerSeries.mul_invOfUnit {R : Type u_1} [Ring R] (φ : PowerSeries R) (u : Rˣ) (h : (PowerSeries.constantCoeff R) φ = u) :
      φ * φ.invOfUnit u = 1
      @[simp]
      theorem PowerSeries.invOfUnit_mul {R : Type u_1} [Ring R] (φ : PowerSeries R) (u : Rˣ) (h : (PowerSeries.constantCoeff R) φ = u) :
      φ.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] :

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

      Equations
      • PowerSeries.inv = MvPowerSeries.inv
      Instances For
        instance PowerSeries.instInv {k : Type u_2} [Field k] :
        Equations
        • PowerSeries.instInv = { inv := PowerSeries.inv }
        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) φ)⁻¹ * xFinset.antidiagonal n, if x.2 < n then (PowerSeries.coeff k x.1) φ * (PowerSeries.coeff k x.2) φ⁻¹ else 0
        theorem PowerSeries.zero_inv {k : Type u_2} [Field k] :
        0⁻¹ = 0
        @[simp]
        theorem PowerSeries.invOfUnit_eq {k : Type u_2} [Field k] (φ : PowerSeries k) (h : (PowerSeries.constantCoeff k) φ 0) :
        φ.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) :
        φ.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} (h : (PowerSeries.constantCoeff k) φ₃ 0) :
        φ₁ = φ₂ * φ₃⁻¹ φ₁ * φ₃ = φ₂
        theorem PowerSeries.eq_inv_iff_mul_eq_one {k : Type u_2} [Field 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} (h : (PowerSeries.constantCoeff k) ψ 0) :
        ψ⁻¹ = φ φ * ψ = 1
        theorem PowerSeries.mul_inv_rev {k : Type u_2} [Field k] (φ ψ : PowerSeries k) :
        (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹
        Equations
        @[simp]
        theorem PowerSeries.C_inv {k : Type u_2} [Field k] (r : k) :
        @[simp]
        theorem PowerSeries.X_inv {k : Type u_2} [Field k] :
        PowerSeries.X⁻¹ = 0
        theorem PowerSeries.smul_inv {k : Type u_2} [Field k] (r : k) (φ : PowerSeries k) :
        def PowerSeries.firstUnitCoeff {k : Type u_2} [Field k] {f : PowerSeries k} (hf : f 0) :

        firstUnitCoeff is the non-zero coefficient whose index is f.order, seen as a unit of the field. It is obtained using divided_by_X_pow_order, defined in PowerSeries.Order

        Equations
        Instances For

          Inv_divided_by_X_pow_order is the inverse of the element obtained by diving a non-zero power series by the largest power of X dividing it. Useful to create a term of type Units, done in Unit_divided_by_X_pow_order

          Equations
          Instances For

            Unit_of_divided_by_X_pow_order is the unit power series obtained by dividing a non-zero power series by the largest power of X that divides it.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              theorem PowerSeries.Unit_of_divided_by_X_pow_order_nonzero {k : Type u_2} [Field k] {f : PowerSeries k} (hf : f 0) :
              f.Unit_of_divided_by_X_pow_order = PowerSeries.divided_by_X_pow_order hf
              @[deprecated PowerSeries.map.isLocalHom]
              theorem PowerSeries.map.isLocalRingHom {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) [IsLocalHom f] :

              Alias of PowerSeries.map.isLocalHom.

              The maximal ideal of k⟦X⟧ is generated by X.

              Equations
              • PowerSeries.instNormalizationMonoid = { normUnit := fun (f : PowerSeries k) => f.Unit_of_divided_by_X_pow_order⁻¹, normUnit_zero := , normUnit_mul := , normUnit_coe_units := }
              theorem PowerSeries.normUnit_X {k : Type u_2} [Field k] :
              normUnit PowerSeries.X = 1
              theorem PowerSeries.X_eq_normalizeX {k : Type u_2} [Field k] :
              PowerSeries.X = normalize PowerSeries.X

              The ring isomorphism between the residue field of the ring of power series valued in a field K and K itself.

              Equations
              Instances For