Documentation Verification Report

LinearRecurrence

📁 Source: Mathlib/Algebra/LinearRecurrence.lean

Statistics

Metric	Count
Definitions `LinearRecurrence`, `IsSolution`, `charPoly`, `coeffs`, `mkSol`, `solSpace`, `toInit`, `tupleSucc`, `instInhabitedLinearRecurrence`	9
Theorems `charPoly_degree_eq_order`, `charPoly_monic`, `eq_mk_of_is_sol_of_eq_init`, `eq_mk_of_is_sol_of_eq_init'`, `geom_sol_iff_root_charPoly`, `is_sol_iff_mem_solSpace`, `is_sol_mkSol`, `mkSol_eq_init`, `solSpace_rank`, `sol_eq_of_eq_init`	10
Total	19

LinearRecurrence

Definitions

Name	Category	Theorems
`IsSolution` 📖	MathDef	8 math math: `Real.geom_goldenRatio_isSol_fibRec`, `geom_gold_isSol_fibRec`, `Real.geom_goldConj_isSol_fibRec`, `Real.fib_isSol_fibRec`, `geom_sol_iff_root_charPoly`, `is_sol_mkSol`, `is_sol_iff_mem_solSpace`, `Real.geom_goldenConj_isSol_fibRec`
`charPoly` 📖	CompOp	4 math math: `Real.fibRec_charPoly_eq`, `charPoly_monic`, `charPoly_degree_eq_order`, `geom_sol_iff_root_charPoly`
`coeffs` 📖	CompOp	—
`mkSol` 📖	CompOp	4 math math: `eq_mk_of_is_sol_of_eq_init'`, `eq_mk_of_is_sol_of_eq_init`, `mkSol_eq_init`, `is_sol_mkSol`
`solSpace` 📖	CompOp	2 math math: `solSpace_rank`, `is_sol_iff_mem_solSpace`
`toInit` 📖	CompOp	—
`tupleSucc` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`charPoly_degree_eq_order` 📖	mathematical	—	`Polynomial.degree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `charPoly` `WithBot` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne` `order`	—	`charPoly.eq_1` `Polynomial.degree_sub_eq_left_of_degree_lt` `Polynomial.degree_monomial` `one_ne_zero` `NeZero.one` `Finset.sum_congr` `Polynomial.degree_sum_fin_lt`
`charPoly_monic` 📖	mathematical	—	`Polynomial.Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `charPoly`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Polynomial.Monic.eq_1` `Polynomial.leadingCoeff.eq_1` `Polynomial.natDegree_eq_of_degree_eq_some` `charPoly_degree_eq_order` `charPoly.eq_1` `Polynomial.coeff_sub` `Polynomial.coeff_monomial_same` `Polynomial.finset_sum_coeff` `sub_eq_self` `Finset.sum_eq_zero` `Polynomial.coeff_eq_zero_of_degree_lt` `lt_imp_lt_of_le_of_le` `Polynomial.degree_monomial_le` `le_refl` `WithBot.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `WithBot.zeroLEOneClass` `Nat.instZeroLEOneClass` `WithBot.charZero` `Nat.instCharZero`
`eq_mk_of_is_sol_of_eq_init` 📖	mathematical	`IsSolution` `order`	`mkSol`	—	`mkSol.eq_1` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `le_of_not_gt` `add_tsub_cancel_right` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le`
`eq_mk_of_is_sol_of_eq_init'` 📖	mathematical	`IsSolution` `order`	`mkSol`	—	`eq_mk_of_is_sol_of_eq_init`
`geom_sol_iff_root_charPoly` 📖	mathematical	—	`IsSolution` `CommRing.toCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Polynomial.IsRoot` `charPoly`	—	`charPoly.eq_1` `Polynomial.IsRoot.def` `Polynomial.eval.eq_1` `Polynomial.eval₂_sub` `Polynomial.eval₂_monomial` `one_mul` `Polynomial.eval₂_finset_sum` `Finset.sum_congr` `zero_add` `pow_add` `sub_eq_zero` `Finset.mul_sum` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul`
`is_sol_iff_mem_solSpace` 📖	mathematical	—	`IsSolution` `Submodule` `CommSemiring.toSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Pi.Function.module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `solSpace`	—	—
`is_sol_mkSol` 📖	mathematical	—	`IsSolution` `mkSol`	—	`mkSol.eq_1` `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` `Finset.sum_congr` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd`
`mkSol_eq_init` 📖	mathematical	—	`mkSol` `order`	—	`mkSol.eq_1` `Finset.sum_congr`
`solSpace_rank` 📖	mathematical	—	`Module.rank` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Pi.Function.module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `solSpace` `Submodule.addCommMonoid` `Submodule.module` `Cardinal` `Cardinal.instNatCast` `order`	—	`LinearEquiv.rank_eq` `rank_fin_fun`
`sol_eq_of_eq_init` 📖	mathematical	`IsSolution`	`Set.EqOn` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.range` `order`	—	`RingHomInvPair.ids` `Equiv.apply_eq_iff_eq` `LinearEquiv.coe_toEquiv` `Finset.mem_range`

(root)

Definitions

Name	Category	Theorems
`LinearRecurrence` 📖	CompData	—
`instInhabitedLinearRecurrence` 📖	CompOp	—

---

← Back to Index