MvPowerSeries.inv_mul_cancel
theorem MvPowerSeries.inv_mul_cancel :
∀ {σ : Type u_1} {k : Type u_3} [inst : Field k] (φ : MvPowerSeries σ k),
(MvPowerSeries.constantCoeff σ k) φ ≠ 0 → φ⁻¹ * φ = 1
This theorem states that for any type `σ`, any field `k`, and any multivariate formal power series `φ` with coefficients in `k` indexed by `σ`, if the constant coefficient of `φ` is non-zero, then the product of the inverse of `φ` and `φ` itself is equal to 1. In other words, a multivariate formal power series with a non-zero constant coefficient has a multiplicative inverse, meaning it is a unit in the ring of multivariate formal power series. Therefore, this theorem is essentially showing that non-zero constant terms allow for a division operation in the ring of such power series.
More concisely: For any field `k` and multivariate formal power series `φ` over `k` with non-zero constant coefficient, `φ` and its multiplicative inverse `φ⁻¹` satisfy `φ * φ⁻¹ = 1`.
|
MvPowerSeries.invOfUnit_eq
theorem MvPowerSeries.invOfUnit_eq :
∀ {σ : Type u_1} {k : Type u_3} [inst : Field k] (φ : MvPowerSeries σ k)
(h : (MvPowerSeries.constantCoeff σ k) φ ≠ 0),
φ.invOfUnit (Units.mk0 ((MvPowerSeries.constantCoeff σ k) φ) h) = φ⁻¹
The theorem `MvPowerSeries.invOfUnit_eq` states that for any type `σ`, any field `k`, and any multivariate formal power series `φ` over `σ` and `k`, if the constant coefficient of `φ` is non-zero, then `invOfUnit φ` applied to the unit group element created from the constant coefficient of `φ` (using `Units.mk0`) is equal to the multiplicative inverse of `φ` (denoted by `φ⁻¹`). In less technical terms, this theorem is expressing how to calculate the multiplicative inverse of a power series when the constant term is not zero, using the invertibility of the constant term.
More concisely: If `φ` is a multivariate formal power series over a field `k` and `σ` with non-zero constant coefficient, then `Units.mk0 (const coeff φ) ^-1 = φ⁻¹`.
|
MvPowerSeries.inv_eq_zero
theorem MvPowerSeries.inv_eq_zero :
∀ {σ : Type u_1} {k : Type u_3} [inst : Field k] {φ : MvPowerSeries σ k},
φ⁻¹ = 0 ↔ (MvPowerSeries.constantCoeff σ k) φ = 0
This theorem states that for any type `σ`, field `k`, and multivariate formal power series `φ` in variables of type `σ` with coefficients in `k`, the inverse of `φ` is zero if and only if the constant coefficient of `φ` is zero. Here, `MvPowerSeries σ k` represents a multivariate power series indexed by type `σ` with coefficients in the field `k`, and `MvPowerSeries.constantCoeff σ k φ` retrieves the constant coefficient of this power series. The theorem is essentially confirming that if the constant term of a multivariate power series in a field is zero, the series has no multiplicative inverse.
More concisely: For any multivariate formal power series φ of type σ with coefficients in a field k, the constant coefficient of φ being zero if and only if φ has no multiplicative inverse.
|
MvPowerSeries.mul_inv_cancel
theorem MvPowerSeries.mul_inv_cancel :
∀ {σ : Type u_1} {k : Type u_3} [inst : Field k] (φ : MvPowerSeries σ k),
(MvPowerSeries.constantCoeff σ k) φ ≠ 0 → φ * φ⁻¹ = 1
The theorem `MvPowerSeries.mul_inv_cancel` states that for any given type `σ`, another type `k` which is a field, and a multivariate power series `φ` of type `σ` with coefficients in `k`, if the constant coefficient of the power series `φ` is not zero, then the product of the power series `φ` and its multiplicative inverse `φ⁻¹`, is equal to 1. In simpler terms, if the constant term of a multivariate power series is not zero, then the power series is invertible, following the standard rule of multiplicative inverses where any non-zero number multiplied by its inverse gives 1.
More concisely: If `φ` is a multivariate power series over a field `k` with non-zero constant coefficient, then `φ * φ⁻¹ = 1`.
|
MvPowerSeries.inv_eq_iff_mul_eq_one
theorem MvPowerSeries.inv_eq_iff_mul_eq_one :
∀ {σ : Type u_1} {k : Type u_3} [inst : Field k] {φ ψ : MvPowerSeries σ k},
(MvPowerSeries.constantCoeff σ k) ψ ≠ 0 → (ψ⁻¹ = φ ↔ φ * ψ = 1)
This theorem states that for any given types `σ` and `k`, where `k` is a field, and for any multivariate power series `φ` and `ψ` over these types, if the constant coefficient of `ψ` is not zero, then `ψ` is the multiplicative inverse of `φ` if and only if the product of `φ` and `ψ` is equal to one. In mathematical terms, if ψ₀ ≠ 0, then ψ⁻¹ = φ if and only if φψ = 1.
More concisely: Given types `σ` and `k` with `k` a field, and multivariate power series `φ` and `ψ` over `σ` with non-zero constant coefficient for `ψ`, then `ψ` is the multiplicative inverse of `φ` if and only if `φψ = 1`.
|
MvPowerSeries.mul_invOfUnit
theorem MvPowerSeries.mul_invOfUnit :
∀ {σ : Type u_1} {R : Type u_2} [inst : Ring R] (φ : MvPowerSeries σ R) (u : Rˣ),
(MvPowerSeries.constantCoeff σ R) φ = ↑u → φ * φ.invOfUnit u = 1
The theorem `MvPowerSeries.mul_invOfUnit` asserts that for any ring `R` and any multivariate formal power series `φ` indexed over a type `σ`, if the constant coefficient of `φ` is an invertible element `u` of the ring `R`, then the product of `φ` and the inverse of `φ` with respect to `u` is equal to one. In other words, if the constant term of a multivariate power series is an invertible element, then the power series is invertible and its inverse is given by `MvPowerSeries.invOfUnit φ u`.
More concisely: If `φ` is a multivariate formal power series over a ring `R` with invertible constant coefficient `u`, then `φ` and `MvPowerSeries.invOfUnit φ u` are multiplicative inverses.
|