Inverse

📁 Source: Mathlib/RingTheory/PowerSeries/Inverse.lean

Statistics

Metric	Count
Definitions `Inv_divided_by_X_pow_order`, `Unit_of_divided_by_X_pow_order`, `firstUnitCoeff`, `instInv`, `instInvOneClass`, `instNormalizationMonoid`, `inv`, `aux`, `invOfUnit`, `residueFieldOfPowerSeries`	10
Theorems `C_inv`, `Inv_divided_by_X_pow_order_leftInv`, `Inv_divided_by_X_pow_order_rightInv`, `Unit_of_divided_by_X_pow_order_nonzero`, `Unit_of_divided_by_X_pow_order_zero`, `X_eq_normalizeX`, `X_inv`, `coeff_inv`, `coeff_invOfUnit`, `coeff_inv_aux`, `constantCoeff_inv`, `constantCoeff_invOfUnit`, `eq_divided_by_X_pow_order_Iff_Unit`, `eq_inv_iff_mul_eq_one`, `eq_mul_inv_iff_mul_eq`, `hasUnitMulPowIrreducibleFactorization`, `instIsDiscreteValuationRing`, `instIsLocalRing`, `instUniqueFactorizationMonoid`, `invOfUnit_eq`, `invOfUnit_eq'`, `invOfUnit_mul`, `inv_eq_iff_mul_eq_one`, `inv_eq_inv_aux`, `inv_eq_zero`, `inv_mul_cancel`, `isNoetherianRing`, `isUnit_divided_by_X_pow_order`, `isUnit_iff_constantCoeff`, `ker_coeff_eq_max_ideal`, `isLocalHom`, `maximalIdeal_eq_span_X`, `mul_invOfUnit`, `mul_inv_cancel`, `mul_inv_rev`, `normUnit_X`, `normalized_count_X_eq_of_coe`, `smul_inv`, `sub_const_eq_X_mul_shift`, `sub_const_eq_shift_mul_X`, `zero_inv`	41
Total	51

PowerSeries

Definitions

Name	Category	Theorems
`Inv_divided_by_X_pow_order` 📖	CompOp	2 math math: `Inv_divided_by_X_pow_order_leftInv`, `Inv_divided_by_X_pow_order_rightInv`
`Unit_of_divided_by_X_pow_order` 📖	CompOp	2 math math: `Unit_of_divided_by_X_pow_order_zero`, `Unit_of_divided_by_X_pow_order_nonzero`
`firstUnitCoeff` 📖	CompOp	—
`instInv` 📖	CompOp	17 math math: `derivative_inv'`, `inv_eq_iff_mul_eq_one`, `eq_mul_inv_iff_mul_eq`, `X_inv`, `constantCoeff_inv`, `mul_inv_cancel`, `mul_inv_rev`, `invOfUnit_eq'`, `zero_inv`, `inv_eq_zero`, `invOfUnit_eq`, `coeff_inv`, `eq_inv_iff_mul_eq_one`, `C_inv`, `inv_eq_inv_aux`, `smul_inv`, `inv_mul_cancel`
`instInvOneClass` 📖	CompOp	—
`instNormalizationMonoid` 📖	CompOp	3 math math: `normUnit_X`, `normalized_count_X_eq_of_coe`, `X_eq_normalizeX`
`inv` 📖	CompOp	—
`invOfUnit` 📖	CompOp	6 math math: `coeff_invOfUnit`, `constantCoeff_invOfUnit`, `mul_invOfUnit`, `invOfUnit_eq'`, `invOfUnit_eq`, `invOfUnit_mul`
`residueFieldOfPowerSeries` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`C_inv` 📖	mathematical	—	`PowerSeries` `instInv` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instSemiring` `RingHom.instFunLike` `C` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero`	—	`MvPowerSeries.C_inv`
`Inv_divided_by_X_pow_order_leftInv` 📖	mathematical	—	`PowerSeries` `MvPowerSeries.instMul` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Inv_divided_by_X_pow_order` `divXPowOrder` `MvPowerSeries.instOne`	—	`mul_comm` `mul_invOfUnit`
`Inv_divided_by_X_pow_order_rightInv` 📖	mathematical	—	`PowerSeries` `MvPowerSeries.instMul` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `divXPowOrder` `Inv_divided_by_X_pow_order` `MvPowerSeries.instOne`	—	`mul_invOfUnit`
`Unit_of_divided_by_X_pow_order_nonzero` 📖	mathematical	—	`Units.val` `PowerSeries` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Unit_of_divided_by_X_pow_order` `divXPowOrder`	—	`Inv_divided_by_X_pow_order_rightInv` `Inv_divided_by_X_pow_order_leftInv`
`Unit_of_divided_by_X_pow_order_zero` 📖	mathematical	—	`Unit_of_divided_by_X_pow_order` `PowerSeries` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Units.instOne`	—	`Inv_divided_by_X_pow_order_rightInv` `Inv_divided_by_X_pow_order_leftInv`
`X_eq_normalizeX` 📖	mathematical	—	`X` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `DFunLike.coe` `MonoidWithZeroHom` `PowerSeries` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero` `CommSemiring.toCommMonoidWithZero` `instCommSemiring` `Semifield.toCommSemiring` `MonoidWithZeroHom.funLike` `normalize` `instNormalizationMonoid`	—	`normUnit_X` `mul_one`
`X_inv` 📖	mathematical	—	`PowerSeries` `instInv` `X` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`MvPowerSeries.X_inv`
`coeff_inv` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.id` `Semiring.toNonAssocSemiring` `PowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `RingHom` `instSemiring` `RingHom.instFunLike` `constantCoeff` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `Finset.sum` `Finset.HasAntidiagonal.antidiagonal` `Nat.instAddMonoid` `Finset.Nat.instHasAntidiagonal` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`inv_eq_inv_aux` `coeff_inv_aux`
`coeff_invOfUnit` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `PowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `invOfUnit` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Units` `Units.instInv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `Finset.sum` `Finset.HasAntidiagonal.antidiagonal` `Nat.instAddMonoid` `Finset.Nat.instHasAntidiagonal` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`coeff_inv_aux`
`coeff_inv_aux` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `PowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `inv.aux` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `Finset.sum` `Finset.HasAntidiagonal.antidiagonal` `Nat.instAddMonoid` `Finset.Nat.instHasAntidiagonal` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`coeff.eq_1` `inv.aux.eq_1` `Nat.instCanonicallyOrderedAdd` `MvPowerSeries.coeff_inv_aux` `Finset.sum_nbij'` `Finsupp.single_injective` `Finsupp.antidiagonal_single` `Finsupp.single_eq_same` `le_or_gt` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `zero_add` `le_of_lt` `LT.lt.not_ge`
`constantCoeff_inv` 📖	mathematical	—	`DFunLike.coe` `RingHom` `PowerSeries` `Semiring.toNonAssocSemiring` `instSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike` `constantCoeff` `instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero`	—	`MvPowerSeries.constantCoeff_inv`
`constantCoeff_invOfUnit` 📖	mathematical	—	`DFunLike.coe` `RingHom` `PowerSeries` `Semiring.toNonAssocSemiring` `instSemiring` `Ring.toSemiring` `RingHom.instFunLike` `constantCoeff` `invOfUnit` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Units` `Units.instInv`	—	`coeff_zero_eq_constantCoeff_apply` `coeff_invOfUnit`
`eq_divided_by_X_pow_order_Iff_Unit` 📖	mathematical	—	`divXPowOrder` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsUnit` `PowerSeries` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring`	—	`isUnit_divided_by_X_pow_order` `order_zero_of_unit` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `X_pow_order_mul_divXPowOrder` `ENat.toNat_zero` `pow_zero` `one_mul`
`eq_inv_iff_mul_eq_one` 📖	mathematical	—	`PowerSeries` `instInv` `MvPowerSeries.instMul` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `MvPowerSeries.instOne`	—	`MvPowerSeries.eq_inv_iff_mul_eq_one`
`eq_mul_inv_iff_mul_eq` 📖	mathematical	—	`PowerSeries` `MvPowerSeries.instMul` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instInv`	—	`MvPowerSeries.eq_mul_inv_iff_mul_eq`
`hasUnitMulPowIrreducibleFactorization` 📖	mathematical	—	`IsDiscreteValuationRing.HasUnitMulPowIrreducibleFactorization` `PowerSeries` `instCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`X_irreducible` `instIsDomain` `Unit_of_divided_by_X_pow_order_nonzero` `X_pow_order_mul_divXPowOrder`
`instIsDiscreteValuationRing` 📖	mathematical	—	`IsDiscreteValuationRing` `PowerSeries` `instCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instIsDomain` `DivisionRing.toRing` `Field.toDivisionRing` `instIsDomain` `Field.toSemifield`	—	`IsDiscreteValuationRing.ofHasUnitMulPowIrreducibleFactorization` `instIsDomain` `instIsDomain` `hasUnitMulPowIrreducibleFactorization`
`instIsLocalRing` 📖	mathematical	—	`IsLocalRing` `PowerSeries` `instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`MvPowerSeries.instIsLocalRing`
`instUniqueFactorizationMonoid` 📖	mathematical	—	`UniqueFactorizationMonoid` `PowerSeries` `CommSemiring.toCommMonoidWithZero` `instCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield`	—	`IsDiscreteValuationRing.HasUnitMulPowIrreducibleFactorization.toUniqueFactorizationMonoid` `IsDomain.toIsCancelMulZero` `instIsDomain` `instIsDomain` `hasUnitMulPowIrreducibleFactorization`
`invOfUnit_eq` 📖	mathematical	—	`invOfUnit` `DivisionRing.toRing` `Field.toDivisionRing` `DivisionSemiring.toGroupWithZero` `Semifield.toDivisionSemiring` `Field.toSemifield` `DFunLike.coe` `RingHom` `PowerSeries` `Semiring.toNonAssocSemiring` `instSemiring` `DivisionSemiring.toSemiring` `RingHom.instFunLike` `constantCoeff` `instInv`	—	—
`invOfUnit_eq'` 📖	mathematical	`DFunLike.coe` `RingHom` `PowerSeries` `Semiring.toNonAssocSemiring` `instSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike` `constantCoeff` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`invOfUnit` `DivisionRing.toRing` `Field.toDivisionRing` `instInv`	—	`MvPowerSeries.invOfUnit_eq'`
`invOfUnit_mul` 📖	mathematical	`DFunLike.coe` `RingHom` `PowerSeries` `Semiring.toNonAssocSemiring` `instSemiring` `Ring.toSemiring` `RingHom.instFunLike` `constantCoeff` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`MvPowerSeries.instMul` `invOfUnit` `MvPowerSeries.instOne`	—	`MvPowerSeries.invOfUnit_mul`
`inv_eq_iff_mul_eq_one` 📖	mathematical	—	`PowerSeries` `instInv` `MvPowerSeries.instMul` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `MvPowerSeries.instOne`	—	`MvPowerSeries.inv_eq_iff_mul_eq_one`
`inv_eq_inv_aux` 📖	mathematical	—	`PowerSeries` `instInv` `inv.aux` `DivisionRing.toRing` `Field.toDivisionRing` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `instSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.instFunLike` `constantCoeff`	—	—
`inv_eq_zero` 📖	mathematical	—	`PowerSeries` `instInv` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `instSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike` `constantCoeff`	—	`MvPowerSeries.inv_eq_zero`
`inv_mul_cancel` 📖	mathematical	—	`PowerSeries` `MvPowerSeries.instMul` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instInv` `MvPowerSeries.instOne`	—	`MvPowerSeries.inv_mul_cancel`
`isNoetherianRing` 📖	mathematical	—	`IsNoetherianRing` `PowerSeries` `instSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`PrincipalIdealRing.isNoetherianRing` `IsDiscreteValuationRing.toIsPrincipalIdealRing` `instIsDomain` `instIsDomain` `instIsDiscreteValuationRing`
`isUnit_divided_by_X_pow_order` 📖	mathematical	—	`IsUnit` `PowerSeries` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `divXPowOrder`	—	`Inv_divided_by_X_pow_order_rightInv` `Inv_divided_by_X_pow_order_leftInv`
`isUnit_iff_constantCoeff` 📖	mathematical	—	`IsUnit` `PowerSeries` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Ring.toSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `constantCoeff`	—	`MvPowerSeries.isUnit_iff_constantCoeff`
`ker_coeff_eq_max_ideal` 📖	mathematical	—	`RingHom.ker` `PowerSeries` `RingHom` `Semiring.toNonAssocSemiring` `instSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike` `RingHom.instRingHomClass` `constantCoeff` `IsLocalRing.maximalIdeal` `instCommSemiring` `Semifield.toCommSemiring` `instIsLocalRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `ValuationRing.isLocalRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `ValuationRing.toPreValuationRing` `instIsDomain` `ValuationRing.of_field`	—	`Ideal.ext` `RingHom.instRingHomClass` `instIsLocalRing` `ValuationRing.isLocalRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `ValuationRing.toPreValuationRing` `instIsDomain` `ValuationRing.of_field` `RingHom.mem_ker` `maximalIdeal_eq_span_X` `Ideal.mem_span_singleton` `X_dvd_iff`
`maximalIdeal_eq_span_X` 📖	mathematical	—	`IsLocalRing.maximalIdeal` `PowerSeries` `instCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `instIsLocalRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `ValuationRing.isLocalRing` `IsLocalRing.toNontrivial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.instIsLocalRing` `ValuationRing.toPreValuationRing` `instIsDomain` `ValuationRing.of_field` `Ideal.span` `CommSemiring.toSemiring` `Set` `Set.instSingletonSet` `X`	—	`Ideal.isMaximal_iff` `Ideal.mem_span_singleton` `Prime.not_dvd_one` `X_prime` `instIsDomain` `sub_sub_cancel` `Ideal.sub_mem` `X_dvd_iff` `map_sub` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `constantCoeff_C` `coeff_zero_eq_constantCoeff_apply` `sub_eq_zero` `coeff_zero_eq_constantCoeff` `Ideal.eq_top_iff_one` `Ideal.eq_top_of_isUnit_mem` `IsUnit.map` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `Ne.isUnit` `instIsLocalRing` `ValuationRing.isLocalRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `ValuationRing.toPreValuationRing` `ValuationRing.of_field` `IsLocalRing.eq_maximalIdeal`
`mul_invOfUnit` 📖	mathematical	`DFunLike.coe` `RingHom` `PowerSeries` `Semiring.toNonAssocSemiring` `instSemiring` `Ring.toSemiring` `RingHom.instFunLike` `constantCoeff` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`MvPowerSeries.instMul` `invOfUnit` `MvPowerSeries.instOne`	—	`MvPowerSeries.mul_invOfUnit`
`mul_inv_cancel` 📖	mathematical	—	`PowerSeries` `MvPowerSeries.instMul` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instInv` `MvPowerSeries.instOne`	—	`MvPowerSeries.mul_inv_cancel`
`mul_inv_rev` 📖	mathematical	—	`PowerSeries` `instInv` `MvPowerSeries.instMul` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`MvPowerSeries.mul_inv_rev`
`normUnit_X` 📖	mathematical	—	`NormalizationMonoid.normUnit` `PowerSeries` `CommSemiring.toCommMonoidWithZero` `instCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `instNormalizationMonoid` `X` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Units` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Units.instOne`	—	`Unit_of_divided_by_X_pow_order_nonzero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `divXPowOrder_X`
`normalized_count_X_eq_of_coe` 📖	mathematical	—	`Multiset.count` `PowerSeries` `X` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `UniqueFactorizationMonoid.normalizedFactors` `CommSemiring.toCommMonoidWithZero` `instCommSemiring` `Semifield.toCommSemiring` `instNormalizationMonoid` `instUniqueFactorizationMonoid` `Polynomial.toPowerSeries` `Polynomial` `Polynomial.instDecidableEq` `Polynomial.X` `Polynomial.commSemiring` `Polynomial.instNormalizationMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsDomain.to_noZeroDivisors` `instIsDomain` `NormalizedGCDMonoid.toNormalizationMonoid` `CommRing.toCommSemiring` `CommGroupWithZero.instNormalizedGCDMonoid` `Semifield.toCommGroupWithZero` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `Polynomial.commRing` `Polynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `AddGroup.toAddCancelMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `EuclideanDomain.to_principal_ideal_domain` `Polynomial.instEuclideanDomain`	—	`eq_of_forall_le_iff` `instUniqueFactorizationMonoid` `IsDomain.to_noZeroDivisors` `instIsDomain` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `Polynomial.instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `EuclideanDomain.to_principal_ideal_domain` `Nat.cast_le` `IsOrderedAddMonoid.toAddLeftMono` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `Polynomial.X_eq_normalize` `X_eq_normalizeX` `UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors` `Polynomial.irreducible_X` `X_irreducible` `Polynomial.coeff_coe`
`smul_inv` 📖	mathematical	—	`PowerSeries` `instInv` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `instSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `instAlgebra` `Algebra.id` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero`	—	`MvPowerSeries.smul_inv`
`sub_const_eq_X_mul_shift` 📖	mathematical	—	`PowerSeries` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `instAddGroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `instSemiring` `RingHom.instFunLike` `C` `constantCoeff` `MvPowerSeries.instMul` `X` `LinearMap` `RingHom.id` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff`	—	`sub_eq_iff_eq_add` `eq_X_mul_shift_add_const`
`sub_const_eq_shift_mul_X` 📖	mathematical	—	`PowerSeries` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `instAddGroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `instSemiring` `RingHom.instFunLike` `C` `constantCoeff` `MvPowerSeries.instMul` `LinearMap` `RingHom.id` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `X`	—	`sub_eq_iff_eq_add` `eq_shift_mul_X_add_const`
`zero_inv` 📖	mathematical	—	`PowerSeries` `instInv` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`MvPowerSeries.zero_inv`

PowerSeries.inv

Definitions

Name	Category	Theorems
`aux` 📖	CompOp	2 math math: `PowerSeries.coeff_inv_aux`, `PowerSeries.inv_eq_inv_aux`

PowerSeries.map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLocalHom` 📖	mathematical	—	`IsLocalHom` `PowerSeries` `RingHom` `Semiring.toNonAssocSemiring` `PowerSeries.instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `RingHom.instFunLike` `PowerSeries.map`	—	`MvPowerSeries.map.isLocalHom`

---

← Back to Index