Documentation Verification Report

Sequence

📁 Source: Mathlib/Algebra/Polynomial/Sequence.lean

Statistics

Metric	Count
Definitions `Sequence`, `basis`, `coeFun`, `elems'`	4
Theorems `basis_degree_strictMono`, `basis_eq_self`, `basis_natDegree_strictMono`, `degree_eq`, `degree_eq'`, `degree_strictMono`, `linearIndependent`, `natDegree_eq`, `natDegree_strictMono`, `ne_zero`, `span`	11
Total	15

Polynomial

Definitions

Name	Category	Theorems
`Sequence` 📖	CompData	—

Polynomial.Sequence

Definitions

Name	Category	Theorems
`basis` 📖	CompOp	3 math math: `basis_natDegree_strictMono`, `basis_eq_self`, `basis_degree_strictMono`
`coeFun` 📖	CompOp	—
`elems'` 📖	CompOp	6 math math: `degree_eq'`, `natDegree_strictMono`, `degree_eq`, `natDegree_eq`, `degree_strictMono`, `linearIndependent`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`basis_degree_strictMono` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Polynomial.leadingCoeff` `elems'`	`StrictMono` `WithBot` `Nat.instPreorder` `WithBot.instPreorder` `Polynomial` `Polynomial.degree` `DFunLike.coe` `Module.Basis` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Polynomial.ring` `Polynomial.module` `Semiring.toModule` `Module.Basis.instFunLike` `basis`	—	`basis_eq_self` `degree_eq` `WithBot.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `WithBot.zeroLEOneClass` `Nat.instZeroLEOneClass` `WithBot.charZero` `Nat.instCharZero`
`basis_eq_self` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Polynomial.leadingCoeff` `elems'`	`DFunLike.coe` `Module.Basis` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Polynomial.ring` `Polynomial.module` `Semiring.toModule` `Module.Basis.instFunLike` `basis`	—	`Module.Basis.mk_apply` `linearIndependent`
`basis_natDegree_strictMono` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Polynomial.leadingCoeff` `elems'`	`StrictMono` `Nat.instPreorder` `Polynomial` `Polynomial.natDegree` `DFunLike.coe` `Module.Basis` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Polynomial.ring` `Polynomial.module` `Semiring.toModule` `Module.Basis.instFunLike` `basis`	—	`basis_eq_self` `natDegree_eq`
`degree_eq` 📖	mathematical	—	`Polynomial.degree` `elems'` `WithBot` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne`	—	`degree_eq'`
`degree_eq'` 📖	mathematical	—	`Polynomial.degree` `elems'` `WithBot` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne`	—	—
`degree_strictMono` 📖	mathematical	—	`StrictMono` `WithBot` `Nat.instPreorder` `WithBot.instPreorder` `Polynomial` `Polynomial.degree` `elems'`	—	`degree_eq` `WithBot.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `WithBot.zeroLEOneClass` `Nat.instZeroLEOneClass` `WithBot.charZero` `Nat.instCharZero`
`linearIndependent` 📖	mathematical	—	`LinearIndependent` `Polynomial` `Ring.toSemiring` `elems'` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Polynomial.ring` `Polynomial.module` `Semiring.toModule`	—	`linearIndependent_iff'` `Finset.le_sup` `smul_eq_zero_iff_left` `Polynomial.instIsTorsionFree` `instIsTorsionFree` `IsDomain.toIsCancelMulZero` `ne_zero` `Polynomial.degree_eq_bot` `eq_bot_mono` `smul_ne_zero_iff` `IsRegular.right` `IsRegular.of_ne_zero` `Polynomial.degree_smul_of_isRightRegular_leadingCoeff` `degree_eq` `WithBot.charZero` `Nat.instCharZero` `Polynomial.degree_ne_bot` `Polynomial.degree_sum_eq_of_disjoint` `Eq.trans_ne` `ne_of_ne_of_eq`
`natDegree_eq` 📖	mathematical	—	`Polynomial.natDegree` `elems'`	—	`Polynomial.natDegree_eq_of_degree_eq_some` `degree_eq`
`natDegree_strictMono` 📖	mathematical	—	`StrictMono` `Nat.instPreorder` `Polynomial` `Polynomial.natDegree` `elems'`	—	`natDegree_eq`
`ne_zero` 📖	—	—	—	—	`Polynomial.degree_ne_bot` `degree_eq`
`span` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Polynomial.leadingCoeff` `elems'`	`Submodule.span` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Polynomial.ring` `Polynomial.module` `Semiring.toModule` `Set.range` `Top.top` `Submodule` `Submodule.instTop`	—	`Submodule.eq_top_iff'` `Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Subsingleton.eq_zero` `Unique.instSubsingleton` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `Nat.strong_induction_on` `isUnit_iff_exists` `Submodule.subset_span` `Submodule.smul_mem` `smul_assoc` `Polynomial.isScalarTower` `IsScalarTower.left` `sub_eq_iff_eq_add` `zero_add` `Submodule.sub_mem_iff_left` `Polynomial.natDegree_lt_iff_degree_lt` `Polynomial.leadingCoeff_smul_of_smul_regular` `IsSMulRegular.of_mul_eq_one` `IsRegular.right` `isRegular_one` `Polynomial.degree_smul_of_isRightRegular_leadingCoeff` `left_ne_zero_of_mul_eq_one` `IsUnit.isRegular` `Polynomial.leadingCoeff_ne_zero` `Polynomial.degree_eq_natDegree` `degree_eq` `Polynomial.coeff_natDegree` `WithBot.charZero` `Nat.instCharZero` `natDegree_eq` `Polynomial.coeff_smul` `smul_eq_mul` `Nat.cast_one` `mul_one` `Polynomial.degree_sub_lt`

---

← Back to Index