Documentation Verification Report

Schroder

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

Statistics

Metric	Count
Definitions `largeSchroderSeries`	1
Theorems `coeff_X_mul_largeSchroderSeries`, `coeff_X_mul_largeSchroderSeriesSeries_sq`, `coeff_largeSchroderSeries`, `constantCoeff_largeSchroderSeries`, `largeSchroderSeries_eq_one_add_X_mul_largeSchroderSeries_add_X_mul_largeSchroderSeries_sq`	5
Total	6

PowerSeries

Definitions

Name	Category	Theorems
`largeSchroderSeries` 📖	CompOp	5 math math: `coeff_X_mul_largeSchroderSeries`, `coeff_X_mul_largeSchroderSeriesSeries_sq`, `largeSchroderSeries_eq_one_add_X_mul_largeSchroderSeries_add_X_mul_largeSchroderSeries_sq`, `coeff_largeSchroderSeries`, `constantCoeff_largeSchroderSeries`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeff_X_mul_largeSchroderSeries` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Nat.instSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `PowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `MvPowerSeries.instMul` `X` `largeSchroderSeries` `Nat.largeSchroder`	—	`coeff_mul` `Finset.sum_congr` `coeff_largeSchroderSeries` `Finset.Nat.sum_antidiagonal_eq_sum_range_succ` `coeff_X` `ite_mul` `one_mul` `MulZeroClass.zero_mul` `Finset.sum_ite_eq'` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Nat.instCanonicallyOrderedAdd`
`coeff_X_mul_largeSchroderSeriesSeries_sq` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Nat.instSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `PowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `MvPowerSeries.instMul` `X` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `largeSchroderSeries` `Finset.sum` `Nat.instAddCommMonoid` `Finset.range` `Nat.largeSchroder`	—	`pow_two` `mul_assoc` `coeff_mul` `Finset.Nat.sum_antidiagonal_eq_sum_range_succ` `Finset.sum_range_succ` `Finset.sum_congr` `coeff_largeSchroderSeries` `coeff_X_mul_largeSchroderSeries` `tsub_self` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `Nat.largeSchroder_zero` `mul_one` `coeff_zero_eq_constantCoeff` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `constantCoeff_X` `constantCoeff_largeSchroderSeries` `tsub_zero` `MulZeroClass.zero_mul` `IsCancelMulZero.toIsRightCancelMulZero` `Nat.instIsCancelMulZero` `Finset.sum_range_eq_add_Ico` `zero_add` `Finset.sum_Ico_eq_sum_range`
`coeff_largeSchroderSeries` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Nat.instSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `PowerSeries` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `coeff` `largeSchroderSeries` `Nat.largeSchroder`	—	—
`constantCoeff_largeSchroderSeries` 📖	mathematical	—	`DFunLike.coe` `RingHom` `PowerSeries` `Semiring.toNonAssocSemiring` `instSemiring` `Nat.instSemiring` `RingHom.instFunLike` `constantCoeff` `largeSchroderSeries`	—	`coeff_largeSchroderSeries` `Nat.largeSchroder_zero`
`largeSchroderSeries_eq_one_add_X_mul_largeSchroderSeries_add_X_mul_largeSchroderSeries_sq` 📖	mathematical	—	`largeSchroderSeries` `PowerSeries` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiring` `Nat.instSemiring` `MvPowerSeries.instOne` `MvPowerSeries.instMul` `X` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`ext` `coeff_largeSchroderSeries` `Nat.largeSchroder_zero` `coeff_zero_eq_constantCoeff` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `constantCoeff_X` `constantCoeff_largeSchroderSeries` `mul_one` `add_zero` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `one_pow` `SemilinearMapClass.toAddHomClass` `LinearMap.semilinearMapClass` `coeff_one` `zero_add` `coeff_X_mul_largeSchroderSeriesSeries_sq` `coeff_X_mul_largeSchroderSeries` `Nat.largeSchroder_succ` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Finset.sum_congr` `Finset.Iic_eq_Icc` `Nat.bot_eq_zero` `Nat.range_succ_eq_Icc_zero`

---

← Back to Index