Documentation Verification Report

Schroder

📁 Source: Mathlib/Combinatorics/Enumerative/Schroder.lean

Statistics

Metric	Count
Definitions `largeSchroder`, `smallSchroder`	2
Theorems `even_largeSchroder`, `largeSchroder_one`, `largeSchroder_succ`, `largeSchroder_two`, `largeSchroder_zero`, `smallSchroder_one`, `smallSchroder_succ`, `smallSchroder_succ_eq_largeSchroder_div_two`, `smallSchroder_zero`, `two_mul_smallSchroder_succ`	10
Total	12

Nat

Definitions

Name	Category	Theorems
`largeSchroder` 📖	CompOp	10 math math: `largeSchroder_two`, `two_mul_smallSchroder_succ`, `PowerSeries.coeff_X_mul_largeSchroderSeries`, `largeSchroder_succ`, `smallSchroder_succ_eq_largeSchroder_div_two`, `largeSchroder_one`, `PowerSeries.coeff_X_mul_largeSchroderSeriesSeries_sq`, `PowerSeries.coeff_largeSchroderSeries`, `even_largeSchroder`, `largeSchroder_zero`
`smallSchroder` 📖	CompOp	5 math math: `two_mul_smallSchroder_succ`, `smallSchroder_succ_eq_largeSchroder_div_two`, `smallSchroder_one`, `smallSchroder_zero`, `smallSchroder_succ`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`even_largeSchroder` 📖	mathematical	—	`Even` `largeSchroder`	—	—
`largeSchroder_one` 📖	mathematical	—	`largeSchroder`	—	`largeSchroder.eq_2` `largeSchroder_zero` `Finset.sum_congr` `Finset.univ_unique` `tsub_self` `instCanonicallyOrderedAdd` `instOrderedSub` `mul_one` `Finset.sum_const` `Finset.card_singleton`
`largeSchroder_succ` 📖	mathematical	—	`largeSchroder` `Finset.sum` `instAddCommMonoid` `Finset.Iic` `instPreorder` `LocallyFiniteOrder.toLocallyFiniteOrderBot` `instOrderBot` `instLocallyFiniteOrder`	—	`largeSchroder.eq_2` `Finset.sum_congr` `instNoMaxOrder` `Iio_eq_range`
`largeSchroder_two` 📖	mathematical	—	`largeSchroder`	—	`largeSchroder.eq_2` `largeSchroder_one` `Finset.sum_congr` `Fin.sum_univ_two` `largeSchroder_zero` `tsub_zero` `instOrderedSub` `one_mul` `tsub_self` `instCanonicallyOrderedAdd` `mul_one`
`largeSchroder_zero` 📖	mathematical	—	`largeSchroder`	—	—
`smallSchroder_one` 📖	mathematical	—	`smallSchroder`	—	—
`smallSchroder_succ` 📖	mathematical	—	`smallSchroder` `Finset.sum` `instAddCommMonoid` `Finset.Ioo` `instPreorder` `instLocallyFiniteOrder`	—	`instCanonicallyOrderedAdd` `zero_add` `instAtLeastTwoHAddOfNat` `zero_lt_two` `instZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `two_mul_smallSchroder_succ` `instCharZero` `largeSchroder_succ` `Finset.Icc_bot` `Finset.sum_Ioc_add_eq_sum_Icc` `covariant_swap_add_of_covariant_add` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Finset.sum_Ioo_add_eq_sum_Ioc` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `instNoMaxOrder` `tsub_self` `instOrderedSub` `largeSchroder_zero` `mul_one` `tsub_zero` `one_mul` `Finset.sum_congr` `mul_mul_mul_comm`
`smallSchroder_succ_eq_largeSchroder_div_two` 📖	mathematical	—	`smallSchroder` `largeSchroder`	—	—
`smallSchroder_zero` 📖	mathematical	—	`smallSchroder`	—	—
`two_mul_smallSchroder_succ` 📖	mathematical	—	`smallSchroder` `largeSchroder`	—	`smallSchroder_succ_eq_largeSchroder_div_two` `instAtLeastTwoHAddOfNat` `Even.two_dvd` `even_largeSchroder`

---

← Back to Index