Documentation Verification Report

StructurePolynomial

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

Statistics

Metric	Count
Definitions `termW_1`, `termW__1`, `wittStructureInt`, `wittStructureRat`	4
Theorems `C_p_pow_dvd_bind₁_rename_wittPolynomial_sub_sum`, `bind₁_rename_expand_wittPolynomial`, `constantCoeff_wittStructureInt`, `constantCoeff_wittStructureInt_zero`, `constantCoeff_wittStructureRat`, `constantCoeff_wittStructureRat_zero`, `eq_wittStructureInt`, `map_wittStructureInt`, `wittStructureInt_existsUnique`, `wittStructureInt_prop`, `wittStructureInt_rename`, `wittStructureInt_vars`, `wittStructureRat_existsUnique`, `wittStructureRat_prop`, `wittStructureRat_rec`, `wittStructureRat_rec_aux`, `wittStructureRat_vars`, `witt_structure_prop`	18
Total	22

Witt

Definitions

Name	Category	Theorems
`termW_1` 📖	CompOp	—
`termW__1` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`wittStructureInt` 📖	CompOp	8 math math: `eq_wittStructureInt`, `constantCoeff_wittStructureInt`, `wittStructureInt_prop`, `wittStructureInt_vars`, `witt_structure_prop`, `wittStructureInt_rename`, `map_wittStructureInt`, `constantCoeff_wittStructureInt_zero`
`wittStructureRat` 📖	CompOp	7 math math: `constantCoeff_wittStructureRat`, `wittStructureRat_vars`, `wittStructureRat_prop`, `wittStructureRat_rec`, `wittStructureRat_rec_aux`, `constantCoeff_wittStructureRat_zero`, `map_wittStructureInt`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`C_p_pow_dvd_bind₁_rename_wittPolynomial_sub_sum` 📖	mathematical	`DFunLike.coe` `RingHom` `MvPolynomial` `Int.instCommSemiring` `Rat.commSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.map` `Int.castRingHom` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `Rat.commRing` `wittStructureInt` `wittStructureRat`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `MvPolynomial.instCommRingMvPolynomial` `Int.instCommRing` `MvPolynomial.C` `Monoid.toNatPow` `Nat.instMonoid` `CommRing.toCommSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AlgHom` `MvPolynomial.algebra` `Algebra.id` `AlgHom.funLike` `MvPolynomial.bind₁` `MvPolynomial.rename` `wittPolynomial` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `Finset.range` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Int.instMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`pow_zero` `Nat.cast_one` `bind₁_rename_expand_wittPolynomial` `MvPolynomial.C_dvd_iff_zmod` `map_sub` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `sub_eq_zero` `MvPolynomial.map_bind₁` `MvPolynomial.map_rename` `map_wittPolynomial` `wittPolynomial_zmod_self` `MvPolynomial.map_expand` `MvPolynomial.bind₁.eq_1` `aeval_wittPolynomial` `map_sum` `Finset.sum_congr` `MvPolynomial.C_eq_coe_nat` `Nat.cast_pow` `mul_sub` `pow_add` `add_assoc` `add_comm` `tsub_eq_iff_eq_add_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` `Nat.cast_mul` `mul_dvd_mul_left` `pow_succ'` `tsub_add_eq_add_tsub` `pow_mul` `dvd_sub_pow_of_dvd_sub` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `MvPolynomial.expand_zmod`
`bind₁_rename_expand_wittPolynomial` 📖	mathematical	`DFunLike.coe` `RingHom` `MvPolynomial` `Int.instCommSemiring` `Rat.commSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.map` `Int.castRingHom` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `Rat.commRing` `wittStructureInt` `wittStructureRat`	`AlgHom` `CommRing.toCommSemiring` `Int.instCommRing` `MvPolynomial.algebra` `Algebra.id` `AlgHom.funLike` `MvPolynomial.bind₁` `MvPolynomial.rename` `MvPolynomial.expand` `wittPolynomial`	—	`MvPolynomial.map_injective` `Int.cast_injective` `Rat.instCharZero` `MvPolynomial.rename_expand` `MvPolynomial.map_bind₁` `MvPolynomial.map_expand` `MvPolynomial.map_rename` `map_wittPolynomial` `wittStructureRat_prop` `MvPolynomial.expand_bind₁` `MvPolynomial.eval₂Hom_congr'` `Finset.mem_range` `wittPolynomial_vars` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'`
`constantCoeff_wittStructureInt` 📖	mathematical	`DFunLike.coe` `RingHom` `MvPolynomial` `Int.instCommSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.constantCoeff`	`wittStructureInt`	—	`Rat.instCharZero` `MvPolynomial.constantCoeff_map` `map_wittStructureInt` `constantCoeff_wittStructureRat` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`constantCoeff_wittStructureInt_zero` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `Int.instCommSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.constantCoeff` `wittStructureInt`	—	`Rat.instCharZero` `MvPolynomial.constantCoeff_map` `map_wittStructureInt` `constantCoeff_wittStructureRat_zero`
`constantCoeff_wittStructureRat` 📖	mathematical	`DFunLike.coe` `RingHom` `MvPolynomial` `Rat.commSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.constantCoeff`	`wittStructureRat`	—	`Rat.instCharZero` `MvPolynomial.map_aeval` `MvPolynomial.constantCoeff_comp_algebraMap` `MvPolynomial.constantCoeff_rename` `constantCoeff_wittPolynomial` `MvPolynomial.eval₂Hom_zero'_apply` `constantCoeff_xInTermsOfW`
`constantCoeff_wittStructureRat_zero` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `Rat.commSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.constantCoeff` `wittStructureRat`	—	`Rat.instCharZero` `xInTermsOfW_zero` `MvPolynomial.aeval_X` `MvPolynomial.map_aeval` `MvPolynomial.constantCoeff_comp_algebraMap` `MvPolynomial.constantCoeff_rename` `constantCoeff_wittPolynomial` `MvPolynomial.eval₂Hom_zero'_apply`
`eq_wittStructureInt` 📖	mathematical	`DFunLike.coe` `AlgHom` `MvPolynomial` `Int.instCommSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id` `AlgHom.funLike` `MvPolynomial.bind₁` `wittPolynomial` `Int.instCommRing` `CommRing.toCommSemiring` `MvPolynomial.rename`	`wittStructureInt`	—	`MvPolynomial.map_injective` `Int.cast_injective` `Rat.instCharZero` `map_wittStructureInt` `ExistsUnique.unique` `wittStructureRat_existsUnique` `MvPolynomial.map_bind₁` `map_wittPolynomial` `MvPolynomial.map_rename` `wittStructureRat_prop`
`map_wittStructureInt` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `Int.instCommSemiring` `Rat.commSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.map` `Int.castRingHom` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `Rat.commRing` `wittStructureInt` `wittStructureRat`	—	`Nat.strong_induction_on` `wittStructureInt.eq_1` `MvPolynomial.map_mapRange_eq_iff` `Int.coe_castRingHom` `MvPolynomial.coeff_C_mul` `mul_comm` `mul_div_assoc'` `mul_one` `map_sum` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Finset.sum_congr` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `MvPolynomial.map_C` `Finset.mem_range` `map_wittPolynomial` `MvPolynomial.coeff_map` `Nat.cast_pow` `Int.cast_pow` `Int.cast_natCast` `Rat.instCharZero` `Int.instCharZero` `Rat.den_eq_one_iff` `eq_intCast` `Rat.den_div_intCast_eq_one_iff` `Nat.cast_zero` `pow_ne_zero` `isReduced_of_noZeroDivisors` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.ne_zero` `Fact.out` `MvPolynomial.C_dvd_iff_dvd_coeff` `C_p_pow_dvd_bind₁_rename_wittPolynomial_sub_sum`
`wittStructureInt_existsUnique` 📖	mathematical	—	`ExistsUnique`	—	`wittStructureInt_prop` `eq_wittStructureInt`
`wittStructureInt_prop` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPolynomial` `Int.instCommSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id` `AlgHom.funLike` `MvPolynomial.bind₁` `wittStructureInt` `wittPolynomial` `Int.instCommRing` `CommRing.toCommSemiring` `MvPolynomial.rename`	—	`MvPolynomial.map_injective` `Int.cast_injective` `Rat.instCharZero` `wittStructureRat_prop` `MvPolynomial.map_bind₁` `map_wittStructureInt` `map_wittPolynomial` `MvPolynomial.map_rename`
`wittStructureInt_rename` 📖	mathematical	—	`wittStructureInt` `DFunLike.coe` `AlgHom` `MvPolynomial` `Int.instCommSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id` `AlgHom.funLike` `MvPolynomial.rename`	—	`MvPolynomial.map_injective` `Int.cast_injective` `Rat.instCharZero` `map_wittStructureInt` `MvPolynomial.map_rename` `MvPolynomial.bind₁_rename` `MvPolynomial.rename_bind₁` `MvPolynomial.rename_rename`
`wittStructureInt_vars` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `MvPolynomial.vars` `Int.instCommSemiring` `wittStructureInt` `SProd.sprod` `Finset.instSProd` `Finset.univ` `Finset.range`	—	`Int.cast_injective` `Rat.instCharZero` `MvPolynomial.vars_map_of_injective` `map_wittStructureInt` `wittStructureRat_vars`
`wittStructureRat_existsUnique` 📖	mathematical	—	`ExistsUnique`	—	`wittStructureRat_prop` `Rat.instCharZero` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `bind₁_wittPolynomial_xInTermsOfW` `MvPolynomial.bind₁_X_right` `MvPolynomial.bind₁_bind₁` `MvPolynomial.eval₂Hom_congr` `RingHom.ext_rat` `RingHom.instRingHomClass`
`wittStructureRat_prop` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPolynomial` `Rat.commSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id` `AlgHom.funLike` `MvPolynomial.bind₁` `wittStructureRat` `wittPolynomial` `Rat.commRing` `CommRing.toCommSemiring` `MvPolynomial.rename`	—	`Rat.instCharZero` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `MvPolynomial.bind₁_bind₁` `MvPolynomial.eval₂Hom_congr` `RingHom.ext_rat` `RingHom.instRingHomClass` `bind₁_xInTermsOfW_wittPolynomial` `MvPolynomial.bind₁_X_right`
`wittStructureRat_rec` 📖	mathematical	—	`wittStructureRat` `MvPolynomial` `Rat.commSemiring` `CommRing.toCommSemiring` `Rat.commRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MvPolynomial.instCommRingMvPolynomial` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.C` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AlgHom` `MvPolynomial.algebra` `Algebra.id` `AlgHom.funLike` `MvPolynomial.bind₁` `MvPolynomial.rename` `wittPolynomial` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.range` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Nat.instMonoid`	—	`mul_left_comm` `MvPolynomial.C_mul` `div_mul_cancel₀` `pow_ne_zero` `isReduced_of_noZeroDivisors` `IsStrictOrderedRing.noZeroDivisors` `Rat.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `Nat.cast_ne_zero` `Rat.instCharZero` `Nat.Prime.ne_zero` `Fact.out` `MvPolynomial.C_1` `mul_one` `wittStructureRat_rec_aux`
`wittStructureRat_rec_aux` 📖	mathematical	—	`MvPolynomial` `Rat.commSemiring` `CommRing.toCommSemiring` `Rat.commRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MvPolynomial.instCommRingMvPolynomial` `wittStructureRat` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.C` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AlgHom` `MvPolynomial.algebra` `Algebra.id` `AlgHom.funLike` `MvPolynomial.bind₁` `MvPolynomial.rename` `wittPolynomial` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.range` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Nat.instMonoid`	—	`Rat.instCharZero` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `xInTermsOfW_aux` `wittStructureRat.eq_1` `MvPolynomial.bind₁_C_right` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `MvPolynomial.bind₁_X_right` `Finset.sum_congr` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `map_sum` `AlgHomClass.toRingHomClass`
`wittStructureRat_vars` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `MvPolynomial.vars` `Rat.commSemiring` `wittStructureRat` `SProd.sprod` `Finset.instSProd` `Finset.univ` `Finset.range`	—	`Rat.instCharZero` `wittStructureRat.eq_1` `MvPolynomial.mem_vars_bind₁` `MvPolynomial.mem_vars_rename` `xInTermsOfW_vars_subset` `Finset.mem_range` `wittPolynomial_vars` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'`
`witt_structure_prop` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPolynomial` `CommRing.toCommSemiring` `Int.instCommRing` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id` `Ring.toIntAlgebra` `CommRing.toRing` `AlgHom.funLike` `MvPolynomial.aeval` `RingHom` `Int.instCommSemiring` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `MvPolynomial.map` `Int.castRingHom` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `wittStructureInt` `wittPolynomial` `MvPolynomial.rename`	—	`MvPolynomial.hom_bind₁` `MvPolynomial.eval₂Hom_congr` `RingHom.ext_int` `MvPolynomial.map_rename` `map_wittPolynomial` `wittStructureInt_prop`

---

← Back to Index