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`, `span_degreeLE`, `span_degreeLT`	13
Total	17

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	10 math math: `span_degreeLE`, `span`, `degree_eq'`, `basis_eq_self`, `natDegree_strictMono`, `degree_eq`, `natDegree_eq`, `degree_strictMono`, `linearIndependent`, `span_degreeLT`

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` `Ring.toSemiring` `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` `Ring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Polynomial.ring` `Polynomial.module` `Semiring.toModule` `Module.Basis.instFunLike` `basis` `elems'`	—	`Module.Basis.mk_apply` `linearIndependent`
`basis_natDegree_strictMono` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Polynomial.leadingCoeff` `elems'`	`StrictMono` `Nat.instPreorder` `Polynomial` `Ring.toSemiring` `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` `WithBot.natCast`	—	`degree_eq'`
`degree_eq'` 📖	mathematical	—	`Polynomial.degree` `elems'` `WithBot` `WithBot.natCast`	—	—
`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` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `NoZeroDivisors.toNoZeroSMulDivisors` `IsDomain.to_noZeroDivisors` `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` `Ring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Polynomial.ring` `Polynomial.module` `Semiring.toModule` `Set.range` `elems'` `Top.top` `Submodule` `Submodule.instTop`	—	`Submodule.eq_top_iff'` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `span_degreeLT` `Polynomial.mem_degreeLT` `Polynomial.natDegree_lt_iff_degree_lt` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_lt_of_covariant_le` `Nat.instNoMaxOrder` `Nat.instCanonicallyOrderedAdd` `Submodule.span_mono` `Set.preimage_range`
`span_degreeLE` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Polynomial.leadingCoeff` `elems'`	`Submodule.span` `Polynomial` `Ring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Polynomial.ring` `Polynomial.module` `Semiring.toModule` `Set.image` `elems'` `Set.Iic` `Nat.instPreorder` `Polynomial.degreeLE` `WithBot` `WithBot.natCast`	—	`Set.Iio_succ_eq_Iic` `Nat.instNoMaxOrder` `span_degreeLT` `Order.lt_succ_iff` `Order.succ_eq_add_one`
`span_degreeLT` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Polynomial.leadingCoeff` `elems'`	`Submodule.span` `Polynomial` `Ring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Polynomial.ring` `Polynomial.module` `Semiring.toModule` `Set.image` `elems'` `Set.Iio` `Nat.instPreorder` `Polynomial.degreeLT`	—	`Submodule.span_eq_of_le` `Set.mem_image` `SetLike.mem_coe` `Polynomial.mem_degreeLT` `degree_eq` `Nat.cast_lt` `WithBot.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `WithBot.zeroLEOneClass` `Nat.instZeroLEOneClass` `WithBot.charZero` `Nat.instCharZero` `Set.mem_Iio` `Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Subsingleton.eq_zero` `Unique.instSubsingleton` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `Nat.strong_induction_on` `Polynomial.degree_eq_natDegree` `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.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.coeff_natDegree` `natDegree_eq` `Polynomial.coeff_smul` `smul_eq_mul` `Nat.cast_one` `mul_one` `Polynomial.degree_sub_lt` `Polynomial.natDegree_lt_iff_degree_lt` `lt_imp_lt_of_le_of_le` `le_refl` `le_of_lt`

---

← Back to Index