WellKnown

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

Statistics

Metric	Count
Definitions `cos`, `invOneSubPow`, `invUnitsSub`, `sin`	4
Theorems `coeff_invUnitsSub`, `constantCoeff_invUnitsSub`, `invOneSubPow_add`, `invOneSubPow_eq_inv_one_sub_pow`, `invOneSubPow_inv_eq_one_sub_pow`, `invOneSubPow_inv_zero_eq_one`, `invOneSubPow_val_eq_mk_sub_one_add_choose_of_pos`, `invOneSubPow_val_one_eq_invUnitSub_one`, `invOneSubPow_val_succ_eq_mk_add_choose`, `invOneSubPow_zero`, `invUnitsSub_mul_X`, `invUnitsSub_mul_sub`, `map_cos`, `map_invUnitsSub`, `map_sin`, `mk_add_choose_mul_one_sub_pow_eq_one`, `mk_one_mul_one_sub_eq_one`, `mk_one_pow_eq_mk_choose_add`, `one_sub_pow_add_mul_invOneSubPow_val_eq_one_sub_pow`, `one_sub_pow_mul_invOneSubPow_val_add_eq_invOneSubPow_val`	20
Total	24

PowerSeries

Definitions

Name	Category	Theorems
`cos` 📖	CompOp	1 math math: `map_cos`
`invOneSubPow` 📖	CompOp	12 math math: `invOneSubPow_zero`, `invOneSubPow_inv_eq_one_sub_pow`, `invOneSubPow_inv_zero_eq_one`, `one_sub_pow_add_mul_invOneSubPow_val_eq_one_sub_pow`, `one_sub_pow_mul_invOneSubPow_val_add_eq_invOneSubPow_val`, `Polynomial.coeff_mul_invOneSubPow_eq_hilbertPoly_eval`, `invOneSubPow_add`, `invOneSubPow_val_eq_mk_sub_one_add_choose_of_pos`, `invOneSubPow_eq_inv_one_sub_pow`, `invOneSubPow_val_one_eq_invUnitSub_one`, `rescale_neg_one_invOneSubPow`, `invOneSubPow_val_succ_eq_mk_add_choose`
`invUnitsSub` 📖	CompOp	6 math math: `constantCoeff_invUnitsSub`, `coeff_invUnitsSub`, `invUnitsSub_mul_sub`, `map_invUnitsSub`, `invOneSubPow_val_one_eq_invUnitSub_one`, `invUnitsSub_mul_X`
`sin` 📖	CompOp	1 math math: `map_sin`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeff_invUnitsSub` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `PowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `invUnitsSub` `divp` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Units` `Monoid.toNatPow` `Units.instMonoid`	—	—
`constantCoeff_invUnitsSub` 📖	mathematical	—	`DFunLike.coe` `RingHom` `PowerSeries` `Semiring.toNonAssocSemiring` `instSemiring` `Ring.toSemiring` `RingHom.instFunLike` `constantCoeff` `invUnitsSub` `divp` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`coeff_zero_eq_constantCoeff_apply` `coeff_invUnitsSub` `zero_add` `pow_one`
`invOneSubPow_add` 📖	mathematical	—	`invOneSubPow` `Units` `PowerSeries` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Units.instMul`	—	`instIsDedekindFiniteMonoid` `mul_comm` `mk_one_mul_one_sub_eq_one` `invOneSubPow_eq_inv_one_sub_pow` `pow_add`
`invOneSubPow_eq_inv_one_sub_pow` 📖	mathematical	—	`invOneSubPow` `Units` `PowerSeries` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Monoid.toNatPow` `Units.instMonoid` `Units.instInv` `Units.mkOfMulEqOne` `instIsDedekindFiniteMonoid` `CommRing.toCommMonoid` `instCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `instAddGroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `MvPowerSeries.instOne` `X` `Pi.instOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMagma.toMul` `NonUnitalNonAssocCommSemiring.toCommMagma` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocCommSemiring` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MulOne.toOne` `mul_comm` `mk_one_mul_one_sub_eq_one`	—	`instIsDedekindFiniteMonoid` `mul_comm` `mk_one_mul_one_sub_eq_one` `pow_zero` `inv_pow` `DivisionMonoid.inv_eq_of_mul` `Units.val_eq_one` `Units.val_mul` `Units.val_pow_eq_pow_val` `Units.inv_val`
`invOneSubPow_inv_eq_one_sub_pow` 📖	mathematical	—	`Units.inv` `PowerSeries` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `invOneSubPow` `Monoid.toNatPow` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `instAddGroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `MvPowerSeries.instOne` `X`	—	`pow_zero`
`invOneSubPow_inv_zero_eq_one` 📖	mathematical	—	`Units.inv` `PowerSeries` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `invOneSubPow` `MvPowerSeries.instOne`	—	`inv_one`
`invOneSubPow_val_eq_mk_sub_one_add_choose_of_pos` 📖	mathematical	—	`Units.val` `PowerSeries` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `invOneSubPow` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Nat.choose`	—	`invOneSubPow.eq_2` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`invOneSubPow_val_one_eq_invUnitSub_one` 📖	mathematical	—	`Units.val` `PowerSeries` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `invOneSubPow` `invUnitsSub` `CommRing.toRing` `Units` `Units.instOne`	—	`zero_add` `pow_one` `Nat.choose_zero_right` `Nat.cast_one` `one_pow` `divp_one`
`invOneSubPow_val_succ_eq_mk_add_choose` 📖	mathematical	—	`Units.val` `PowerSeries` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `invOneSubPow` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Nat.choose`	—	—
`invOneSubPow_zero` 📖	mathematical	—	`invOneSubPow` `Units` `PowerSeries` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Units.instOne`	—	—
`invUnitsSub_mul_X` 📖	mathematical	—	`PowerSeries` `MvPowerSeries.instMul` `Ring.toSemiring` `invUnitsSub` `X` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `instAddGroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `instSemiring` `RingHom.instFunLike` `C` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MvPowerSeries.instOne`	—	`ext` `coeff_zero_eq_constantCoeff` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `constantCoeff_invUnitsSub` `one_divp` `constantCoeff_X` `MulZeroClass.mul_zero` `map_sub` `RingHomClass.toAddMonoidHomClass` `Units.inv_mul` `sub_self` `coeff_succ_mul_X` `coeff_invUnitsSub` `pow_succ'` `mul_inv_rev` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `coeff_mul_C` `Units.inv_mul_cancel_right` `coeff_one` `sub_zero`
`invUnitsSub_mul_sub` 📖	mathematical	—	`PowerSeries` `MvPowerSeries.instMul` `Ring.toSemiring` `invUnitsSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `instAddGroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `instSemiring` `RingHom.instFunLike` `C` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X` `MvPowerSeries.instOne`	—	`mul_sub` `invUnitsSub_mul_X` `sub_sub_cancel`
`map_cos` 📖	mathematical	—	`DFunLike.coe` `RingHom` `PowerSeries` `Semiring.toNonAssocSemiring` `instSemiring` `Ring.toSemiring` `RingHom.instFunLike` `map` `cos`	—	`ext` `RingHom.map_rat_algebraMap` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`map_invUnitsSub` 📖	mathematical	—	`DFunLike.coe` `RingHom` `PowerSeries` `Semiring.toNonAssocSemiring` `instSemiring` `Ring.toSemiring` `RingHom.instFunLike` `map` `invUnitsSub` `MonoidHom` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulOneClass.toMulOne` `Units.instMulOneClass` `MonoidHom.instFunLike` `Units.map` `MonoidHomClass.toMonoidHom` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`	—	`ext` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `coeff_invUnitsSub` `one_divp` `MonoidHom.instMonoidHomClass`
`map_sin` 📖	mathematical	—	`DFunLike.coe` `RingHom` `PowerSeries` `Semiring.toNonAssocSemiring` `instSemiring` `Ring.toSemiring` `RingHom.instFunLike` `map` `sin`	—	`ext` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `RingHom.map_rat_algebraMap`
`mk_add_choose_mul_one_sub_pow_eq_one` 📖	mathematical	—	`PowerSeries` `MvPowerSeries.instMul` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Nat.choose` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `instAddGroup` `AddGroupWithOne.toAddGroup` `MvPowerSeries.instOne` `X`	—	`Units.val_inv`
`mk_one_mul_one_sub_eq_one` 📖	mathematical	—	`PowerSeries` `MvPowerSeries.instMul` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Pi.instOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `instAddGroup` `AddGroupWithOne.toAddGroup` `MvPowerSeries.instOne` `X`	—	`mul_comm` `ext_iff` `coeff_zero_eq_constantCoeff` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `map_sub` `RingHomClass.toAddMonoidHomClass` `constantCoeff_X` `sub_zero` `mul_one` `coeff_one` `sub_mul` `one_mul` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `coeff_succ_X_mul` `sub_self`
`mk_one_pow_eq_mk_choose_add` 📖	mathematical	—	`PowerSeries` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Pi.instOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddMonoidWithOne.toNatCast` `Nat.choose`	—	`ext` `zero_add` `pow_one` `Nat.choose_zero_right` `Nat.cast_one` `pow_add` `mul_comm` `coeff_mul` `Finset.sum_congr` `one_mul` `Nat.cast_sum` `Finset.sum_antidiagonal_choose_add` `add_right_comm`
`one_sub_pow_add_mul_invOneSubPow_val_eq_one_sub_pow` 📖	mathematical	—	`PowerSeries` `MvPowerSeries.instMul` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `instAddGroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `MvPowerSeries.instOne` `X` `Units.val` `invOneSubPow`	—	`pow_add` `invOneSubPow_inv_eq_one_sub_pow` `mul_assoc` `Units.inv_mul` `mul_one`
`one_sub_pow_mul_invOneSubPow_val_add_eq_invOneSubPow_val` 📖	mathematical	—	`PowerSeries` `MvPowerSeries.instMul` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `instAddGroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `MvPowerSeries.instOne` `X` `Units.val` `invOneSubPow`	—	`invOneSubPow_add` `mul_comm` `mul_assoc` `Units.mul_inv` `one_mul`

---

← Back to Index