Documentation Verification Report

HilbertPoly

📁 Source: Mathlib/RingTheory/Polynomial/HilbertPoly.lean

Statistics

Metric	Count
Definitions `hilbertPoly`, `hilbertPoly_linearMap`, `preHilbertPoly`	3
Theorems `coeff_mul_invOneSubPow_eq_hilbertPoly_eval`, `coeff_preHilbertPoly_self`, `eq_hilbertPoly_of_forall_coeff_eq_eval`, `existsUnique_hilbertPoly`, `hilbertPoly_X_pow_succ`, `hilbertPoly_add_left`, `hilbertPoly_eq_zero_of_le_rootMultiplicity_one`, `hilbertPoly_mul_one_sub_pow_add`, `hilbertPoly_mul_one_sub_succ`, `hilbertPoly_smul`, `hilbertPoly_succ`, `hilbertPoly_zero_left`, `hilbertPoly_zero_right`, `leadingCoeff_preHilbertPoly`, `natDegree_hilbertPoly_of_ne_zero`, `natDegree_hilbertPoly_of_ne_zero_of_rootMultiplicity_lt`, `natDegree_preHilbertPoly`, `preHilbertPoly_eq_choose_sub_add`	18
Total	21

Polynomial

Definitions

Name	Category	Theorems
`hilbertPoly` 📖	CompOp	13 math math: `hilbertPoly_smul`, `hilbertPoly_eq_zero_of_le_rootMultiplicity_one`, `natDegree_hilbertPoly_of_ne_zero_of_rootMultiplicity_lt`, `eq_hilbertPoly_of_forall_coeff_eq_eval`, `hilbertPoly_succ`, `hilbertPoly_zero_left`, `hilbertPoly_add_left`, `natDegree_hilbertPoly_of_ne_zero`, `hilbertPoly_X_pow_succ`, `coeff_mul_invOneSubPow_eq_hilbertPoly_eval`, `hilbertPoly_mul_one_sub_succ`, `hilbertPoly_mul_one_sub_pow_add`, `hilbertPoly_zero_right`
`hilbertPoly_linearMap` 📖	CompOp	—
`preHilbertPoly` 📖	CompOp	6 math math: `hilbertPoly_succ`, `preHilbertPoly_eq_choose_sub_add`, `hilbertPoly_X_pow_succ`, `leadingCoeff_preHilbertPoly`, `natDegree_preHilbertPoly`, `coeff_preHilbertPoly_self`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeff_mul_invOneSubPow_eq_hilbertPoly_eval` 📖	mathematical	`natDegree` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `PowerSeries` `PowerSeries.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `PowerSeries.instModule` `Semiring.toModule` `LinearMap.instFunLike` `PowerSeries.coeff` `MvPowerSeries.instMul` `toPowerSeries` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `PowerSeries.instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Field.toCommRing` `PowerSeries.invOneSubPow` `eval` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `hilbertPoly`	—	`PowerSeries.invOneSubPow_zero` `mul_one` `coeff_coe` `eval_zero` `coeff_eq_zero_of_natDegree_lt` `eval_finset_sum` `Finset.sum_congr` `eval_smul` `IsScalarTower.right` `Finset.sum_coe_sort` `le_trans` `le_natDegree_of_ne_zero` `mem_support_iff` `LT.lt.le` `preHilbertPoly_eq_choose_sub_add` `PowerSeries.coeff_mul` `PowerSeries.invOneSubPow_val_eq_mk_sub_one_add_choose_of_pos` `Finset.sum_subset_zero_on_sdiff` `Finset.mem_range_succ_iff` `MulZeroClass.zero_mul` `add_comm` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`coeff_preHilbertPoly_self` 📖	mathematical	—	`coeff` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `preHilbertPoly` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Nat.factorial`	—	`Nat.cast_zero` `ne_of_gt` `Nat.factorial_pos` `natDegree_preHilbertPoly` `natDegree_smul` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `inv_ne_zero` `sub_add` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `coeff_smul` `leadingCoeff_comp` `ne_of_eq_of_ne` `natDegree_X_sub_C` `one_ne_zero` `IsDomain.to_noZeroDivisors` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `Monic.def` `monic_ascPochhammer` `leadingCoeff_X_sub_C` `one_pow` `mul_one`
`eq_hilbertPoly_of_forall_coeff_eq_eval` 📖	mathematical	`DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.id` `Semiring.toNonAssocSemiring` `PowerSeries` `PowerSeries.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `PowerSeries.instModule` `Semiring.toModule` `LinearMap.instFunLike` `PowerSeries.coeff` `MvPowerSeries.instMul` `toPowerSeries` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `PowerSeries.instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Field.toCommRing` `PowerSeries.invOneSubPow` `eval` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	`hilbertPoly`	—	`ExistsUnique.unique` `existsUnique_hilbertPoly` `coeff_mul_invOneSubPow_eq_hilbertPoly_eval`
`existsUnique_hilbertPoly` 📖	mathematical	—	`ExistsUnique` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`coeff_mul_invOneSubPow_eq_hilbertPoly_eval` `eq_of_infinite_eval_eq` `instIsDomain` `Set.Infinite.mono` `Set.Infinite.image` `Function.Injective.injOn` `Nat.cast_injective` `Set.Ioi_infinite` `Nat.instNoMaxOrder`
`hilbertPoly_X_pow_succ` 📖	mathematical	—	`hilbertPoly` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `preHilbertPoly`	—	`Finset.sum_congr` `coeff_X_pow` `ite_smul` `one_smul` `zero_smul` `Finset.sum_ite_eq'` `NeZero.one` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing`
`hilbertPoly_add_left` 📖	mathematical	—	`hilbertPoly` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instAdd`	—	`add_zero` `sum_def` `sum_add_index` `zero_smul` `add_smul`
`hilbertPoly_eq_zero_of_le_rootMultiplicity_one` 📖	mathematical	`rootMultiplicity` `DivisionRing.toRing` `Field.toDivisionRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	`hilbertPoly` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instZero`	—	`hilbertPoly_zero_left` `exists_eq_pow_rootMultiplicity_mul_and_not_dvd` `mul_assoc` `neg_mul` `one_mul` `neg_sub` `mul_comm` `zero_add` `pow_add` `hilbertPoly_mul_one_sub_pow_add` `hilbertPoly.eq_1`
`hilbertPoly_mul_one_sub_pow_add` 📖	mathematical	—	`hilbertPoly` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `instSub` `DivisionRing.toRing` `Field.toDivisionRing` `instOne` `X`	—	`pow_zero` `mul_one` `add_zero` `pow_add` `pow_one` `mul_assoc` `add_assoc` `hilbertPoly_mul_one_sub_succ`
`hilbertPoly_mul_one_sub_succ` 📖	mathematical	—	`hilbertPoly` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instMul` `instSub` `DivisionRing.toRing` `Field.toDivisionRing` `instOne` `X`	—	`eq_hilbertPoly_of_forall_coeff_eq_eval` `coe_sub` `coe_one` `coe_X` `PowerSeries.one_sub_pow_mul_invOneSubPow_val_add_eq_invOneSubPow_val` `pow_one` `mul_assoc` `coe_mul` `coeff_mul_invOneSubPow_eq_hilbertPoly_eval`
`hilbertPoly_smul` 📖	mathematical	—	`hilbertPoly` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Algebra.toSMul` `Semifield.toCommSemiring` `semiring` `algebraOfAlgebra` `Algebra.id`	—	`smul_zero` `sum_def` `smul_sum` `sum_smul_index'` `zero_smul` `smul_assoc` `isScalarTower` `IsScalarTower.right`
`hilbertPoly_succ` 📖	mathematical	—	`hilbertPoly` `Finset.sum` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `Field.toCommRing` `support` `Algebra.toSMul` `Semifield.toCommSemiring` `semiring` `algebraOfAlgebra` `Algebra.id` `coeff` `preHilbertPoly`	—	—
`hilbertPoly_zero_left` 📖	mathematical	—	`hilbertPoly` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instZero`	—	`Finset.sum_congr` `zero_smul` `Finset.sum_const_zero`
`hilbertPoly_zero_right` 📖	mathematical	—	`hilbertPoly` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instZero`	—	—
`leadingCoeff_preHilbertPoly` 📖	mathematical	—	`leadingCoeff` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `preHilbertPoly` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Nat.factorial`	—	`leadingCoeff.eq_1` `natDegree_preHilbertPoly` `coeff_preHilbertPoly_self`
`natDegree_hilbertPoly_of_ne_zero` 📖	mathematical	—	`natDegree` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `hilbertPoly` `rootMultiplicity` `DivisionRing.toRing` `Field.toDivisionRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`hilbertPoly_zero_left` `hilbertPoly_eq_zero_of_le_rootMultiplicity_one` `not_lt` `natDegree_hilbertPoly_of_ne_zero_of_rootMultiplicity_lt`
`natDegree_hilbertPoly_of_ne_zero_of_rootMultiplicity_lt` 📖	mathematical	`rootMultiplicity` `DivisionRing.toRing` `Field.toDivisionRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	`natDegree` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `hilbertPoly`	—	`exists_eq_pow_rootMultiplicity_mul_and_not_dvd` `mul_assoc` `neg_mul` `one_mul` `neg_sub` `mul_comm` `le_of_lt` `hilbertPoly_mul_one_sub_pow_add` `natDegree_eq_of_le_of_coeff_ne_zero` `natDegree_sum_le_of_forall_le` `le_trans` `natDegree_smul_le` `natDegree_preHilbertPoly` `le_refl` `one_pow` `mul_one` `finset_sum_coeff` `Finset.sum_congr` `coeff_smul` `coeff_preHilbertPoly_self` `sum_def` `eval_mul` `eval_pow` `eval_neg` `eval_one` `IsDomain.to_noZeroDivisors` `instIsDomain` `isReduced_of_noZeroDivisors` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `NeZero.charZero_one` `not_iff_not` `dvd_iff_isRoot` `Nat.factorial_ne_zero`
`natDegree_preHilbertPoly` 📖	mathematical	—	`natDegree` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `preHilbertPoly`	—	`Nat.cast_zero` `ne_of_gt` `Nat.factorial_pos` `preHilbertPoly.eq_1` `natDegree_smul` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `inv_ne_zero` `natDegree_comp` `IsDomain.to_noZeroDivisors` `ascPochhammer_natDegree` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `add_comm_sub` `C_1` `map_sub` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `natDegree_add_C` `natDegree_X` `mul_one`
`preHilbertPoly_eq_choose_sub_add` 📖	mathematical	—	`eval` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `preHilbertPoly` `Nat.choose`	—	`Nat.cast_zero` `ne_of_gt` `Nat.factorial_pos` `map_natCast` `RingHom.instRingHomClass` `eval_smul` `IsScalarTower.right` `eval_comp` `eval_add` `eval_sub` `eval_X` `eval_natCast` `eval_one` `Nat.cast_add` `Nat.cast_sub` `Nat.cast_one` `ascPochhammer_nat_eq_natCast_ascFactorial` `Nat.ascFactorial_eq_factorial_mul_choose` `Nat.cast_mul` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `one_mul` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial`

---

← Back to Index