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	10 math math: eq_wittStructureInt, constantCoeff_wittStructureInt, wittStructureInt_prop, wittStructureInt_vars, bind₁_rename_expand_wittPolynomial, witt_structure_prop, wittStructureInt_rename, map_wittStructureInt, C_p_pow_dvd_bind₁_rename_wittPolynomial_sub_sum, 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 AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike MvPolynomial.map Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing Rat.commRing wittStructureInt wittStructureRat	MvPolynomial Int.instCommSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero AddMonoidAlgebra.nonUnitalSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring AddMonoid.toAddSemigroup Finsupp.instAddMonoid Nat.instAddMonoid DFunLike.coe RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass RingHom.instFunLike MvPolynomial.C Monoid.toPow Nat.instMonoid CommRing.toCommSemiring Int.instCommRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidAlgebra.ring Int.instRing AlgHom AddMonoidAlgebra.semiring AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike MvPolynomial.bind₁ MvPolynomial.rename wittPolynomial Finset.sum AddMonoidAlgebra.addAddCommMonoid Finset.range AddMonoidAlgebra.instMul Finsupp.instAdd Int.instMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero wittStructureInt	—	pow_zero Nat.cast_one eq_intCast RingHom.instRingHomClass Int.cast_one wittPolynomial_zero MvPolynomial.rename_X Finset.sum_congr Int.cast_pow Int.cast_natCast zero_tsub Nat.instCanonicallyOrderedAdd Nat.instOrderedSub pow_one sub_zero bind₁_rename_expand_wittPolynomial MvPolynomial.C_dvd_iff_zmod map_sub RingHomClass.toAddMonoidHomClass 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 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 IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid 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 AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid RingHom.instFunLike MvPolynomial.map Int.castRingHom NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing Rat.commRing wittStructureInt wittStructureRat	DFunLike.coe AlgHom MvPolynomial CommRing.toCommSemiring Int.instCommRing AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike MvPolynomial.bind₁ MvPolynomial.rename MvPolynomial.expand wittPolynomial Int.instCommSemiring wittStructureInt	—	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 AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike MvPolynomial.constantCoeff	DFunLike.coe RingHom MvPolynomial Int.instCommSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring 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 AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike MvPolynomial.constantCoeff wittStructureInt	—	Rat.instCharZero MvPolynomial.constantCoeff_map map_wittStructureInt constantCoeff_wittStructureRat_zero
constantCoeff_wittStructureRat 📖	mathematical	DFunLike.coe RingHom MvPolynomial Rat.commSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike MvPolynomial.constantCoeff	DFunLike.coe RingHom MvPolynomial Rat.commSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring 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 AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring 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 AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.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 AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid 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 AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.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 AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.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 AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.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 AddMonoidAlgebra.instMul Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid DFunLike.coe RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass RingHom.instFunLike MvPolynomial.C SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidAlgebra.ring DivisionRing.toRing Rat.instDivisionRing Finsupp.instAddMonoid AlgHom AddMonoidAlgebra.semiring AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike MvPolynomial.bind₁ MvPolynomial.rename wittPolynomial Finset.sum AddMonoidAlgebra.addAddCommMonoid Finset.range Monoid.toPow 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 AddMonoidAlgebra.instMul Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid wittStructureRat DFunLike.coe RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass RingHom.instFunLike MvPolynomial.C SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidAlgebra.ring DivisionRing.toRing Rat.instDivisionRing Finsupp.instAddMonoid AlgHom AddMonoidAlgebra.semiring AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike MvPolynomial.bind₁ MvPolynomial.rename wittPolynomial Finset.sum AddMonoidAlgebra.addAddCommMonoid Finset.range Monoid.toPow 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 AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.commSemiring Finsupp.instAddCommMonoid Nat.instAddCommMonoid AddMonoidAlgebra.algebra Algebra.id Ring.toIntAlgebra CommRing.toRing AddCommMonoid.toAddMonoid AlgHom.funLike MvPolynomial.aeval RingHom Int.instCommSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass 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