Inverse

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

Statistics

Metric	Count
Definitions `instInv`, `instInvOneClass`, `inv`, `aux`, `invOfUnit`	5
Theorems `C_inv`, `X_inv`, `coeff_inv`, `coeff_invOfUnit`, `coeff_inv_aux`, `constantCoeff_inv`, `constantCoeff_invOfUnit`, `eq_inv_iff_mul_eq_one`, `eq_mul_inv_iff_mul_eq`, `instIsLocalRing`, `invOfUnit_eq`, `invOfUnit_eq'`, `invOfUnit_mul`, `inv_eq_iff_mul_eq_one`, `inv_eq_zero`, `inv_mul_cancel`, `isUnit_iff_constantCoeff`, `isLocalHom`, `mul_invOfUnit`, `mul_inv_cancel`, `mul_inv_rev`, `smul_inv`, `zero_inv`	23
Total	28

MvPowerSeries

Definitions

Name	Category	Theorems
`instInv` 📖	CompOp	15 math math: `zero_inv`, `eq_inv_iff_mul_eq_one`, `inv_eq_iff_mul_eq_one`, `constantCoeff_inv`, `coeff_inv`, `inv_mul_cancel`, `C_inv`, `inv_eq_zero`, `X_inv`, `mul_inv_cancel`, `invOfUnit_eq'`, `eq_mul_inv_iff_mul_eq`, `invOfUnit_eq`, `mul_inv_rev`, `smul_inv`
`instInvOneClass` 📖	CompOp	—
`inv` 📖	CompOp	—
`invOfUnit` 📖	CompOp	6 math math: `constantCoeff_invOfUnit`, `invOfUnit_mul`, `coeff_invOfUnit`, `mul_invOfUnit`, `invOfUnit_eq'`, `invOfUnit_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`C_inv` 📖	mathematical	—	`MvPowerSeries` `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`	—	`eq_or_ne` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `zero_inv` `inv_zero` `inv_eq_iff_mul_eq_one` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `inv_mul_cancel₀` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass`
`X_inv` 📖	mathematical	—	`MvPowerSeries` `instInv` `X` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	—	`inv_eq_zero` `constantCoeff_X`
`coeff_inv` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `instInv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instZero` `Finsupp.instDecidableEq` `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` `Field.toCommRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `Finset.sum` `Finset.HasAntidiagonal.antidiagonal` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Finsupp.instHasAntidiagonal` `Preorder.toLT` `Finsupp.preorder` `Nat.instPreorder` `Finsupp.decidableLT` `Nat.instAddCommMonoid` `Nat.instPartialOrder` `Nat.instCanonicallyOrderedAdd` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`coeff_inv_aux`
`coeff_invOfUnit` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `invOfUnit` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instZero` `Finsupp.instDecidableEq` `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` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Finsupp.instHasAntidiagonal` `Preorder.toLT` `Finsupp.preorder` `Nat.instPreorder` `Finsupp.decidableLT` `Nat.instAddCommMonoid` `Nat.instPartialOrder` `Nat.instCanonicallyOrderedAdd` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Nat.instCanonicallyOrderedAdd` `Finset.sum_congr` `coeff_inv_aux`
`coeff_inv_aux` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `MvPowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `inv.aux` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instZero` `Finsupp.instDecidableEq` `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` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Finsupp.instHasAntidiagonal` `Preorder.toLT` `Finsupp.preorder` `Nat.instPreorder` `Finsupp.decidableLT` `Nat.instAddCommMonoid` `Nat.instPartialOrder` `Nat.instCanonicallyOrderedAdd` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Nat.instCanonicallyOrderedAdd` `inv.aux.eq_1`
`constantCoeff_inv` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPowerSeries` `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`	—	`coeff_zero_eq_constantCoeff_apply` `Nat.instCanonicallyOrderedAdd` `coeff_inv`
`constantCoeff_invOfUnit` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPowerSeries` `Semiring.toNonAssocSemiring` `instSemiring` `Ring.toSemiring` `RingHom.instFunLike` `constantCoeff` `invOfUnit` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Units` `Units.instInv`	—	`coeff_zero_eq_constantCoeff_apply` `Nat.instCanonicallyOrderedAdd` `coeff_invOfUnit`
`eq_inv_iff_mul_eq_one` 📖	mathematical	—	`MvPowerSeries` `instInv` `instMul` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instOne`	—	`eq_mul_inv_iff_mul_eq` `one_mul`
`eq_mul_inv_iff_mul_eq` 📖	mathematical	—	`MvPowerSeries` `instMul` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instInv`	—	`mul_assoc` `inv_mul_cancel` `mul_one` `mul_inv_cancel`
`instIsLocalRing` 📖	mathematical	—	`IsLocalRing` `MvPowerSeries` `instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`IsLocalRing.of_isUnit_or_isUnit_one_sub_self` `instNontrivial` `IsLocalRing.toNontrivial` `IsLocalRing.isUnit_or_isUnit_one_sub_self` `IsUnit.of_mul_eq_one` `instIsDedekindFiniteMonoid` `mul_invOfUnit` `map_sub` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass`
`invOfUnit_eq` 📖	mathematical	—	`invOfUnit` `DivisionRing.toRing` `Field.toDivisionRing` `DivisionSemiring.toGroupWithZero` `Semifield.toDivisionSemiring` `Field.toSemifield` `DFunLike.coe` `RingHom` `MvPowerSeries` `Semiring.toNonAssocSemiring` `instSemiring` `DivisionSemiring.toSemiring` `RingHom.instFunLike` `constantCoeff` `instInv`	—	—
`invOfUnit_eq'` 📖	mathematical	`DFunLike.coe` `RingHom` `MvPowerSeries` `Semiring.toNonAssocSemiring` `instSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike` `constantCoeff` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`invOfUnit` `DivisionRing.toRing` `Field.toDivisionRing` `instInv`	—	`Units.ne_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `invOfUnit_eq` `Units.ext_iff`
`invOfUnit_mul` 📖	mathematical	`DFunLike.coe` `RingHom` `MvPowerSeries` `Semiring.toNonAssocSemiring` `instSemiring` `Ring.toSemiring` `RingHom.instFunLike` `constantCoeff` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`instMul` `invOfUnit` `instOne`	—	`mul_cancel_right_mem_nonZeroDivisors` `mem_nonZeroDivisors_of_constantCoeff` `constantCoeff_invOfUnit` `IsUnit.mem_nonZeroDivisors` `Units.isUnit` `mul_assoc` `one_mul` `mul_invOfUnit` `mul_one`
`inv_eq_iff_mul_eq_one` 📖	mathematical	—	`MvPowerSeries` `instInv` `instMul` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instOne`	—	`eq_inv_iff_mul_eq_one`
`inv_eq_zero` 📖	mathematical	—	`MvPowerSeries` `instInv` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `instSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike` `constantCoeff`	—	`constantCoeff_inv` `ext` `Nat.instCanonicallyOrderedAdd` `coeff_inv` `inv_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `neg_zero` `MulZeroClass.zero_mul`
`inv_mul_cancel` 📖	mathematical	—	`MvPowerSeries` `instMul` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instInv` `instOne`	—	`mul_comm` `mul_inv_cancel`
`isUnit_iff_constantCoeff` 📖	mathematical	—	`IsUnit` `MvPowerSeries` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Ring.toSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `constantCoeff`	—	`IsUnit.map` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `mul_invOfUnit` `invOfUnit_mul`
`mul_invOfUnit` 📖	mathematical	`DFunLike.coe` `RingHom` `MvPowerSeries` `Semiring.toNonAssocSemiring` `instSemiring` `Ring.toSemiring` `RingHom.instFunLike` `constantCoeff` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`instMul` `invOfUnit` `instOne`	—	`ext` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `constantCoeff_invOfUnit` `Units.mul_inv` `Finset.HasAntidiagonal.mem_antidiagonal` `zero_add` `coeff_one` `coeff_mul` `Finset.insert_erase` `Finset.sum_insert` `Finset.notMem_erase` `coeff_zero_eq_constantCoeff_apply` `Nat.instCanonicallyOrderedAdd` `coeff_invOfUnit` `neg_mul` `mul_neg` `Units.mul_inv_cancel_left` `not_lt_of_ge` `le_rfl` `add_comm` `sub_eq_add_neg` `sub_eq_zero` `Finset.sum_congr` `Finset.mem_erase` `lt_add_of_pos_left` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `Finsupp.instIsRightCancelAdd` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Finsupp.isOrderedAddMonoid` `Nat.instIsOrderedAddMonoid` `pos_iff_ne_zero` `Finsupp.instCanonicallyOrderedAddOfAddLeftMono` `Nat.instOrderedSub`
`mul_inv_cancel` 📖	mathematical	—	`MvPowerSeries` `instMul` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instInv` `instOne`	—	`invOfUnit_eq` `mul_invOfUnit`
`mul_inv_rev` 📖	mathematical	—	`MvPowerSeries` `instInv` `instMul` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`inv_eq_zero` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `IsDomain.to_noZeroDivisors` `Field.isDomain` `MulZeroClass.mul_zero` `MulZeroClass.zero_mul` `inv_eq_iff_mul_eq_one` `mul_assoc` `inv_mul_cancel` `mul_one`
`smul_inv` 📖	mathematical	—	`MvPowerSeries` `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`	—	`smul_eq_C_mul` `mul_comm` `mul_inv_rev` `C_inv`
`zero_inv` 📖	mathematical	—	`MvPowerSeries` `instInv` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	—	`inv_eq_zero` `constantCoeff_zero`

MvPowerSeries.inv

Definitions

Name	Category	Theorems
`aux` 📖	CompOp	1 math math: `MvPowerSeries.coeff_inv_aux`

MvPowerSeries.map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLocalHom` 📖	mathematical	—	`IsLocalHom` `MvPowerSeries` `RingHom` `Semiring.toNonAssocSemiring` `MvPowerSeries.instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `RingHom.instFunLike` `MvPowerSeries.map`	—	`MvPowerSeries.isUnit_constantCoeff` `Units.isUnit` `isUnit_of_map_unit` `MvPowerSeries.constantCoeff_map` `IsUnit.of_mul_eq_one` `instIsDedekindFiniteMonoid` `MvPowerSeries.mul_invOfUnit`

---

← Back to Index