Documentation Verification Report

WittPolynomial

📁 Source: Mathlib/RingTheory/WittVector/WittPolynomial.lean

Statistics

Metric	Count
Definitions `termW`, `termW_`, `wittPolynomial`, `xInTermsOfW`	4
Theorems `aeval_wittPolynomial`, `bind₁_wittPolynomial_xInTermsOfW`, `bind₁_xInTermsOfW_wittPolynomial`, `constantCoeff_wittPolynomial`, `constantCoeff_xInTermsOfW`, `map_wittPolynomial`, `wittPolynomial_eq_sum_C_mul_X_pow`, `wittPolynomial_one`, `wittPolynomial_vars`, `wittPolynomial_vars_subset`, `wittPolynomial_zero`, `wittPolynomial_zmod_self`, `xInTermsOfW_aux`, `xInTermsOfW_eq`, `xInTermsOfW_vars_aux`, `xInTermsOfW_vars_subset`, `xInTermsOfW_zero`	17
Total	21

Witt

Definitions

Name	Category	Theorems
`termW` 📖	CompOp	—
`termW_` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`wittPolynomial` 📖	CompOp	28 math math: `WittVector.bind₁_frobeniusPoly_wittPolynomial`, `wittPolynomial_zmod_self`, `WittVector.ghostComponent_apply`, `aeval_wittPolynomial`, `bind₁_xInTermsOfW_wittPolynomial`, `wittPolynomial_one`, `wittPolynomial_vars`, `WittVector.mul_polyOfInterest_aux4`, `wittPolynomial_vars_subset`, `WittVector.bind₁_wittMulN_wittPolynomial`, `wittStructureRat_prop`, `wittStructureRat_rec`, `wittStructureRat_rec_aux`, `wittStructureInt_prop`, `constantCoeff_wittPolynomial`, `bind₁_rename_expand_wittPolynomial`, `witt_structure_prop`, `WittVector.bind₁_verschiebungPoly_wittPolynomial`, `WittVector.polyOfInterest_vars_eq`, `WittVector.bind₁_onePoly_wittPolynomial`, `map_wittPolynomial`, `WittVector.bind₁_zero_wittPolynomial`, `wittPolynomial_zero`, `bind₁_wittPolynomial_xInTermsOfW`, `WittVector.bind₁_frobeniusPolyRat_wittPolynomial`, `WittVector.mul_polyOfInterest_aux3`, `C_p_pow_dvd_bind₁_rename_wittPolynomial_sub_sum`, `wittPolynomial_eq_sum_C_mul_X_pow`
`xInTermsOfW` 📖	CompOp	8 math math: `bind₁_xInTermsOfW_wittPolynomial`, `xInTermsOfW_eq`, `xInTermsOfW_aux`, `xInTermsOfW_zero`, `xInTermsOfW_vars_subset`, `xInTermsOfW_vars_aux`, `bind₁_wittPolynomial_xInTermsOfW`, `constantCoeff_xInTermsOfW`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aeval_wittPolynomial` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPolynomial` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id` `AlgHom.funLike` `MvPolynomial.aeval` `wittPolynomial` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finset.range` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Nat.instMonoid`	—	`map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Finset.sum_congr` `MvPolynomial.aeval_monomial` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `map_natCast` `Finsupp.prod_single_index` `pow_zero`
`bind₁_wittPolynomial_xInTermsOfW` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPolynomial` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id` `AlgHom.funLike` `MvPolynomial.bind₁` `wittPolynomial` `xInTermsOfW` `MvPolynomial.X`	—	`xInTermsOfW_eq` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `MvPolynomial.bind₁_X_right` `MvPolynomial.algHom_C` `map_sum` `mul_assoc` `MvPolynomial.C_mul` `mul_pow` `mul_invOf_self` `one_pow` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `mul_one` `wittPolynomial_eq_sum_C_mul_X_pow` `Finset.sum_range_succ_comm` `tsub_self` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `pow_zero` `pow_one` `mul_comm` `add_sub_assoc` `add_eq_left` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `sub_eq_zero` `Finset.sum_congr` `map_pow` `AlgHomClass.toRingHomClass` `Finset.mem_range` `MvPolynomial.algebraMap_eq`
`bind₁_xInTermsOfW_wittPolynomial` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPolynomial` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id` `AlgHom.funLike` `MvPolynomial.bind₁` `xInTermsOfW` `wittPolynomial` `MvPolynomial.X`	—	`wittPolynomial_eq_sum_C_mul_X_pow` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Finset.sum_congr` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHomClass.toRingHomClass` `MvPolynomial.algHom_C` `Finset.sum_range_succ_comm` `tsub_self` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `pow_zero` `pow_one` `MvPolynomial.bind₁_X_right` `mul_comm` `MvPolynomial.C_pow` `xInTermsOfW_aux` `sub_add_cancel`
`constantCoeff_wittPolynomial` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `CommRing.toCommSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.constantCoeff` `wittPolynomial` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`map_sum` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Finset.sum_congr` `MvPolynomial.constantCoeff_monomial` `Finset.sum_eq_zero` `Finsupp.single_eq_zero` `ne_of_gt` `pow_pos` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `Nat.instZeroLEOneClass` `Nat.Prime.pos` `Fact.out`
`constantCoeff_xInTermsOfW` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `CommRing.toCommSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.constantCoeff` `xInTermsOfW` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`xInTermsOfW_eq` `mul_comm` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `map_sub` `RingHomClass.toAddMonoidHomClass` `map_sum` `MvPolynomial.constantCoeff_C` `MvPolynomial.constantCoeff_X` `zero_sub` `mul_neg` `neg_eq_zero` `Finset.sum_eq_zero` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `map_natCast` `Finset.mem_range` `zero_pow` `pow_ne_zero` `isReduced_of_noZeroDivisors` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.ne_zero` `Fact.out` `MulZeroClass.mul_zero`
`map_wittPolynomial` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `CommRing.toCommSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.map` `wittPolynomial`	—	`wittPolynomial.eq_1` `map_sum` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Finset.sum_congr` `MvPolynomial.map_monomial` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `map_natCast`
`wittPolynomial_eq_sum_C_mul_X_pow` 📖	mathematical	—	`wittPolynomial` `Finset.sum` `MvPolynomial` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MvPolynomial.instCommRingMvPolynomial` `Finset.range` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `MvPolynomial.X` `Nat.instMonoid`	—	`Finset.sum_congr` `MvPolynomial.monomial_eq` `Finsupp.prod_single_index` `pow_zero`
`wittPolynomial_one` 📖	mathematical	—	`wittPolynomial` `MvPolynomial` `CommRing.toCommSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MvPolynomial.instCommRingMvPolynomial` `Distrib.toMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.C` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `MvPolynomial.X` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`wittPolynomial_eq_sum_C_mul_X_pow` `Finset.sum_range_succ_comm` `pow_one` `tsub_self` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `pow_zero` `Finset.sum_singleton` `tsub_zero` `one_mul`
`wittPolynomial_vars` 📖	mathematical	—	`MvPolynomial.vars` `CommRing.toCommSemiring` `wittPolynomial` `Finset.range`	—	`MvPolynomial.vars_monomial_single` `pow_ne_zero` `isReduced_of_noZeroDivisors` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `Nat.cast_pow` `Nat.cast_ne_zero` `wittPolynomial.eq_1` `MvPolynomial.vars_sum_of_disjoint` `Finset.disjoint_singleton_left` `Finset.mem_singleton` `Finset.biUnion_singleton_eq_self`
`wittPolynomial_vars_subset` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `MvPolynomial.vars` `CommRing.toCommSemiring` `wittPolynomial` `Finset.range`	—	`map_wittPolynomial` `wittPolynomial_vars` `Int.instCharZero` `MvPolynomial.vars_map`
`wittPolynomial_zero` 📖	mathematical	—	`wittPolynomial` `MvPolynomial.X` `CommRing.toCommSemiring`	—	`Finset.sum_congr` `zero_add` `Finset.sum_singleton` `tsub_self` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `pow_zero`
`wittPolynomial_zmod_self` 📖	mathematical	—	`wittPolynomial` `ZMod` `Monoid.toNatPow` `Nat.instMonoid` `ZMod.commRing` `DFunLike.coe` `AlgHom` `MvPolynomial` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id` `AlgHom.funLike` `MvPolynomial.expand`	—	`wittPolynomial_eq_sum_C_mul_X_pow` `Finset.sum_range_succ` `Nat.cast_pow` `CharP.cast_eq_zero` `ZMod.charP` `MvPolynomial.C_0` `MulZeroClass.zero_mul` `add_zero` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Finset.sum_congr` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `MvPolynomial.expand_X` `MvPolynomial.algHom_C` `pow_mul` `pow_succ'` `add_comm` `add_tsub_assoc_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `Finset.mem_range`
`xInTermsOfW_aux` 📖	mathematical	—	`MvPolynomial` `CommRing.toCommSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MvPolynomial.instCommRingMvPolynomial` `xInTermsOfW` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `MvPolynomial.X` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.range` `Nat.instMonoid`	—	`xInTermsOfW_eq` `mul_assoc` `MvPolynomial.C_mul` `mul_pow` `invOf_mul_self` `one_pow` `MvPolynomial.C_1` `mul_one`
`xInTermsOfW_eq` 📖	mathematical	—	`xInTermsOfW` `MvPolynomial` `CommRing.toCommSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MvPolynomial.instCommRingMvPolynomial` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `MvPolynomial.X` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.range` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Nat.instMonoid` `Invertible.invOf` `AddMonoidWithOne.toOne`	—	`xInTermsOfW.eq_1` `Fin.sum_univ_eq_sum_range`
`xInTermsOfW_vars_aux` 📖	mathematical	—	`Finset` `Finset.instMembership` `MvPolynomial.vars` `CommRing.toCommSemiring` `Rat.commRing` `xInTermsOfW` `invertibleOfPos` `Field.toSemifield` `Rat.instField` `Rat.instCharZero` `NeZero.of_gt'` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPreorder` `Nat.instCanonicallyOrderedAdd` `Nat.instOne` `Nat.Prime.one_lt'` `Finset.instHasSubset` `Finset.range`	—	`Rat.instCharZero` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `xInTermsOfW_eq` `mul_comm` `MvPolynomial.vars_C_mul` `IsStrictOrderedRing.noZeroDivisors` `Rat.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `Invertible.ne_zero` `Rat.nontrivial` `MvPolynomial.vars_sub_of_disjoint` `MvPolynomial.vars_X` `Finset.disjoint_singleton_left` `MvPolynomial.vars_sum_subset` `Finset.mem_biUnion` `Finset.mem_range` `MvPolynomial.vars_pow` `pow_ne_zero` `isReduced_of_noZeroDivisors` `Nat.cast_zero` `Nat.Prime.ne_zero` `Fact.out` `Finset.range_add_one` `Finset.insert_eq` `Finset.mem_union`
`xInTermsOfW_vars_subset` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `MvPolynomial.vars` `CommRing.toCommSemiring` `Rat.commRing` `xInTermsOfW` `invertibleOfPos` `Field.toSemifield` `Rat.instField` `Rat.instCharZero` `NeZero.of_gt'` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPreorder` `Nat.instCanonicallyOrderedAdd` `Nat.instOne` `Nat.Prime.one_lt'` `Finset.range`	—	`Rat.instCharZero` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `xInTermsOfW_vars_aux`
`xInTermsOfW_zero` 📖	mathematical	—	`xInTermsOfW` `MvPolynomial.X` `CommRing.toCommSemiring`	—	`xInTermsOfW_eq` `Finset.range_zero` `Finset.sum_empty` `pow_zero` `MvPolynomial.C_1` `mul_one` `sub_zero`

---

← Back to Index