OAI/NumberTheory/Catalan/Determinants/FixedCompactRow38.lean
14 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.InternalCatalan.fixedRowPData_38line 12 - def
OAI.InternalCatalan.fixedRowPCoeff_38line 51 - theorem
OAI.InternalCatalan.fixed_rowP_typed_coeff_38line 90 - theorem
OAI.InternalCatalan.fixed_rowP_typed_tail_38line 94 - theorem
OAI.InternalCatalan.fixed_rowP_typed_scalar_38line 98 - theorem
OAI.InternalCatalan.fixed_rowP_typed_factor_38line 102 - theorem
OAI.InternalCatalan.fixed_rowP_typed_38line 128 - def
OAI.InternalCatalan.fixedRowDData_38line 136 - def
OAI.InternalCatalan.fixedRowDCoeff_38line 173 - theorem
OAI.InternalCatalan.fixed_rowD_typed_coeff_38line 210 - theorem
OAI.InternalCatalan.fixed_rowD_typed_tail_38line 214 - theorem
OAI.InternalCatalan.fixed_rowD_typed_scalar_38line 218 - theorem
OAI.InternalCatalan.fixed_rowD_typed_factor_38line 222 - theorem
OAI.InternalCatalan.fixed_rowD_typed_38line 248