Defs

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

Statistics

Metric	Count
Definitions WittVector, coeff, eval, hasIntScalar, hasNatPow, hasNatScalar, instAdd, instFunctor, instInhabited, instIntCast, instMul, instNatCast, instNeg, instOne, instSub, instZero, mk, peval, wittAdd, wittMul, wittNSMul, wittNeg, wittOne, wittPow, wittSub, wittZSMul, wittZero	27
Theorems add_coeff, add_coeff_zero, coeff_mk, coeff_surjective, constantCoeff_wittAdd, constantCoeff_wittMul, constantCoeff_wittNSMul, constantCoeff_wittNeg, constantCoeff_wittSub, constantCoeff_wittZSMul, ext, ext_iff, instLawfulFunctor, mul_coeff, mul_coeff_zero, neg_coeff, nsmul_coeff, one_coeff_eq_of_pos, one_coeff_zero, pow_coeff, sub_coeff, v2_coeff, wittAdd_vars, wittAdd_zero, wittMul_vars, wittMul_zero, wittNSMul_vars, wittNeg_vars, wittNeg_zero, wittOne_pos_eq_zero, wittOne_zero_eq_one, wittPow_vars, wittSub_vars, wittSub_zero, wittZSMul_vars, wittZero_eq_zero, zero_coeff, zsmul_coeff	38
Total	65

WittVector

Definitions

Name	Category	Theorems
coeff 📖	CompOp	72 math math: aeval_verschiebung_poly', coeff_truncate, teichmuller_mul_pow_coeff_of_ne, coeff_surjective, ghostComponent_apply, RecursionMain.succNthVal_spec', zsmul_coeff, verschiebung_coeff_succ, map_coeff, pow_coeff, coeff_p, TruncatedWittVector.coeff_out, mulN_coeff, mem_span_p_pow_iff_le_coeff_eq_zero, IsPoly₂.poly, mem_ker_truncate, verschiebungFun_coeff, matrix_vecEmpty_coeff, IsPoly.poly, coeff_truncateFun, iterate_verschiebung_coeff_eq_zero, dvd_sub_sum_teichmuller_iterateFrobeniusEquiv_coeff, verschiebung_coeff_zero, iterate_frobenius_coeff, zero_coeff, coeff_frobenius_charP, sub_coeff, mul_coeff, coeff_frobeniusFun, RecursionBase.solution_spec, one_coeff_zero, coeff_mk, coeff_p_pow, mul_pow_charP_coeff_zero, shift_coeff, one_coeff_eq_of_pos, verschiebungFun_coeff_zero, iterate_verschiebung_mul_coeff, coeff_p_zero, coeff_select, map_eq_zero_iff, nth_mul_coeff, v2_coeff, teichmuller_coeff_zero, RecursionBase.solution_pow, mul_coeff_zero, iterate_verschiebung_coeff, verschiebungFun_coeff_succ, RecursionBase.solution_spec', neg_coeff, verschiebung_coeff_add_one, ext_iff, teichmuller_mul_pow_coeff, aeval_verschiebungPoly, peval_polyOfInterest', constantCoeff_apply, nthRemainder_spec, coeff_p_pow_eq_zero, mem_span_p_iff_coeff_zero_eq_zero, mul_charP_coeff_zero, teichmuller_coeff_pos, mk_fontaineTheta, add_coeff_zero, add_coeff, coeff_frobenius, mul_pow_charP_coeff_succ, le_coeff_eq_iff_le_sub_coeff_eq_zero, coeff_p_one, nsmul_coeff, nth_mul_coeff', peval_polyOfInterest, mul_charP_coeff_succ
eval 📖	CompOp	—
hasIntScalar 📖	CompOp	4 math math: zsmul_coeff, init_zsmul, mapFun.zsmul, truncateFun_zsmul
hasNatPow 📖	CompOp	15 math math: teichmuller_mul_pow_coeff_of_ne, init_pow, pow_coeff, mapFun.pow, mem_span_p_pow_iff_le_coeff_eq_zero, truncateFun_pow, exists_eq_pow_p_mul', dvd_sub_sum_teichmuller_iterateFrobeniusEquiv_coeff, iterate_verschiebung_iterate_frobenius, coeff_p_pow, mul_pow_charP_coeff_zero, exists_eq_pow_p_mul, teichmuller_mul_pow_coeff, coeff_p_pow_eq_zero, mul_pow_charP_coeff_succ
hasNatScalar 📖	CompOp	4 math math: mapFun.nsmul, truncateFun_nsmul, init_nsmul, nsmul_coeff
instAdd 📖	CompOp	12 math math: mapFun.add, coeff_add_of_disjoint, frobeniusEquiv_symm_apply, truncateFun_add, init_add, select_add_select_not, addIsPoly₂, frobeniusEquiv_apply, ghostEquiv_coe, add_coeff_zero, add_coeff, init_add_tail
instFunctor 📖	CompOp	1 math math: instLawfulFunctor
instInhabited 📖	CompOp	—
instIntCast 📖	CompOp	2 math math: truncateFun_intCast, mapFun.intCast
instMul 📖	CompOp	35 math math: teichmuller_mul_pow_coeff_of_ne, verschiebung_zmod, frobeniusEquiv_symm_apply, iterate_verschiebung_mul, instNoZeroDivisorsOfCharP, frobenius_frobeniusRotation, mulN_coeff, init_mul, mapFun.mul, mulIsPoly₂, exists_eq_pow_p_mul', dvd_sub_sum_teichmuller_iterateFrobeniusEquiv_coeff, iterate_verschiebung_iterate_frobenius, verschiebung_mul_frobenius, mul_coeff, verschiebung_frobenius, mul_pow_charP_coeff_zero, iterate_verschiebung_mul_coeff, nth_mul_coeff, truncateFun_mul, exists_eq_pow_p_mul, iterate_verschiebung_mul_left, mul_coeff_zero, mulN_isPoly, frobeniusEquiv_apply, teichmuller_mul_pow_coeff, peval_polyOfInterest', nthRemainder_spec, mul_charP_coeff_zero, ghostEquiv_coe, mul_pow_charP_coeff_succ, frobenius_verschiebung, nth_mul_coeff', peval_polyOfInterest, mul_charP_coeff_succ
instNatCast 📖	CompOp	28 math math: teichmuller_mul_pow_coeff_of_ne, verschiebung_zmod, coeff_p, mulN_coeff, mem_span_p_pow_iff_le_coeff_eq_zero, exists_eq_pow_p_mul', dvd_sub_sum_teichmuller_iterateFrobeniusEquiv_coeff, irreducible, iterate_verschiebung_iterate_frobenius, isAdicCompleteIdealSpanP, verschiebung_frobenius, coeff_p_pow, mul_pow_charP_coeff_zero, truncateFun_natCast, quotientPEquiv_mk, coeff_p_zero, exists_eq_pow_p_mul, mulN_isPoly, ker_constantCoeff, teichmuller_mul_pow_coeff, coeff_p_pow_eq_zero, mem_span_p_iff_coeff_zero_eq_zero, mul_charP_coeff_zero, mul_pow_charP_coeff_succ, frobenius_verschiebung, mapFun.natCast, coeff_p_one, mul_charP_coeff_succ
instNeg 📖	CompOp	5 math math: negIsPoly, init_neg, truncateFun_neg, neg_coeff, mapFun.neg
instOne 📖	CompOp	5 math math: mapFun.one, truncateFun_one, oneIsPoly, one_coeff_zero, one_coeff_eq_of_pos
instSub 📖	CompOp	6 math math: mapFun.sub, dvd_sub_sum_teichmuller_iterateFrobeniusEquiv_coeff, sub_coeff, init_sub, truncateFun_sub, le_coeff_eq_iff_le_sub_coeff_eq_zero
instZero 📖	CompOp	7 math math: mapFun.zero, teichmuller_zero, truncateFun_zero, instNoZeroDivisorsOfCharP, zeroIsPoly, zero_coeff, map_eq_zero_iff
mk 📖	CompOp	—
peval 📖	CompOp	10 math math: zsmul_coeff, pow_coeff, IsPoly₂.poly, sub_coeff, mul_coeff, neg_coeff, peval_polyOfInterest', add_coeff, nsmul_coeff, peval_polyOfInterest
wittAdd 📖	CompOp	4 math math: wittAdd_vars, constantCoeff_wittAdd, add_coeff, wittAdd_zero
wittMul 📖	CompOp	8 math math: mul_polyOfInterest_aux2, mul_polyOfInterest_aux4, mul_coeff, constantCoeff_wittMul, mul_polyOfInterest_aux1, wittMul_zero, polyOfInterest_vars_eq, wittMul_vars
wittNSMul 📖	CompOp	3 math math: constantCoeff_wittNSMul, wittNSMul_vars, nsmul_coeff
wittNeg 📖	CompOp	4 math math: wittNeg_zero, neg_coeff, constantCoeff_wittNeg, wittNeg_vars
wittOne 📖	CompOp	2 math math: wittOne_zero_eq_one, wittOne_pos_eq_zero
wittPow 📖	CompOp	2 math math: pow_coeff, wittPow_vars
wittSub 📖	CompOp	4 math math: sub_coeff, wittSub_vars, wittSub_zero, constantCoeff_wittSub
wittZSMul 📖	CompOp	3 math math: zsmul_coeff, wittZSMul_vars, constantCoeff_wittZSMul
wittZero 📖	CompOp	1 math math: wittZero_eq_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_coeff 📖	mathematical	—	coeff WittVector instAdd peval wittAdd Matrix.vecCons Matrix.vecEmpty	—	v2_coeff
add_coeff_zero 📖	mathematical	—	coeff WittVector instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	add_coeff wittAdd_zero map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass MvPolynomial.aeval_X Matrix.cons_val' Matrix.cons_val_fin_one
coeff_mk 📖	mathematical	—	coeff	—	—
coeff_surjective 📖	mathematical	—	WittVector coeff	—	—
constantCoeff_wittAdd 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Int.instCommSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.constantCoeff wittAdd	—	constantCoeff_wittStructureInt map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass MvPolynomial.constantCoeff_X add_zero
constantCoeff_wittMul 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Int.instCommSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.constantCoeff wittMul	—	constantCoeff_wittStructureInt map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass MvPolynomial.constantCoeff_X MulZeroClass.mul_zero
constantCoeff_wittNSMul 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Int.instCommSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.constantCoeff wittNSMul	—	constantCoeff_wittStructureInt map_nsmul RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass MvPolynomial.constantCoeff_X smul_zero
constantCoeff_wittNeg 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Int.instCommSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.constantCoeff wittNeg	—	constantCoeff_wittStructureInt map_neg RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass MvPolynomial.constantCoeff_X neg_zero
constantCoeff_wittSub 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Int.instCommSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.constantCoeff wittSub	—	constantCoeff_wittStructureInt map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass MvPolynomial.constantCoeff_X sub_zero
constantCoeff_wittZSMul 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial Int.instCommSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.constantCoeff wittZSMul	—	constantCoeff_wittStructureInt map_zsmul RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass MvPolynomial.constantCoeff_X smul_zero
ext 📖	—	coeff	—	—	—
ext_iff 📖	mathematical	—	coeff	—	ext
instLawfulFunctor 📖	mathematical	—	WittVector instFunctor	—	—
mul_coeff 📖	mathematical	—	coeff WittVector instMul peval wittMul Matrix.vecCons Matrix.vecEmpty	—	v2_coeff
mul_coeff_zero 📖	mathematical	—	coeff WittVector instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	mul_coeff wittMul_zero map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass MvPolynomial.aeval_X Matrix.cons_val' Matrix.cons_val_fin_one
neg_coeff 📖	mathematical	—	coeff WittVector instNeg peval wittNeg Matrix.vecCons Matrix.vecEmpty	—	Matrix.cons_val_fin_one Matrix.cons_fin_one
nsmul_coeff 📖	mathematical	—	coeff WittVector hasNatScalar peval wittNSMul Matrix.vecCons Matrix.vecEmpty	—	Matrix.cons_val_fin_one Matrix.cons_fin_one
one_coeff_eq_of_pos 📖	mathematical	—	coeff WittVector instOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	wittOne_pos_eq_zero map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass
one_coeff_zero 📖	mathematical	—	coeff WittVector instOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	wittOne_zero_eq_one map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass
pow_coeff 📖	mathematical	—	coeff WittVector hasNatPow peval wittPow Matrix.vecCons Matrix.vecEmpty	—	Matrix.cons_val_fin_one Matrix.cons_fin_one
sub_coeff 📖	mathematical	—	coeff WittVector instSub peval wittSub Matrix.vecCons Matrix.vecEmpty	—	v2_coeff
v2_coeff 📖	mathematical	—	coeff Matrix.vecCons WittVector Matrix.vecEmpty	—	Fintype.complete Matrix.cons_val_fin_one
wittAdd_vars 📖	mathematical	—	Finset Finset.instHasSubset MvPolynomial.vars Int.instCommSemiring wittAdd SProd.sprod Finset.instSProd Finset.univ Fin.fintype Finset.range	—	wittStructureInt_vars
wittAdd_zero 📖	mathematical	—	wittAdd MvPolynomial Int.instCommSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing MvPolynomial.instCommRingMvPolynomial Int.instCommRing MvPolynomial.X	—	MvPolynomial.map_injective Int.cast_injective Rat.instCharZero map_wittStructureInt map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass MvPolynomial.map_X SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass MvPolynomial.bind₁_X_right xInTermsOfW_zero wittPolynomial_zero MvPolynomial.rename_X
wittMul_vars 📖	mathematical	—	Finset Finset.instHasSubset MvPolynomial.vars Int.instCommSemiring wittMul SProd.sprod Finset.instSProd Finset.univ Fin.fintype Finset.range	—	wittStructureInt_vars
wittMul_zero 📖	mathematical	—	wittMul MvPolynomial Int.instCommSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing MvPolynomial.instCommRingMvPolynomial Int.instCommRing MvPolynomial.X	—	MvPolynomial.map_injective Int.cast_injective Rat.instCharZero map_wittStructureInt map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass MvPolynomial.map_X NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass MvPolynomial.bind₁_X_right xInTermsOfW_zero wittPolynomial_zero MvPolynomial.rename_X
wittNSMul_vars 📖	mathematical	—	Finset Finset.instHasSubset MvPolynomial.vars Int.instCommSemiring wittNSMul SProd.sprod Finset.instSProd Finset.univ Fin.fintype Finset.range	—	wittStructureInt_vars
wittNeg_vars 📖	mathematical	—	Finset Finset.instHasSubset MvPolynomial.vars Int.instCommSemiring wittNeg SProd.sprod Finset.instSProd Finset.univ Fin.fintype Finset.range	—	wittStructureInt_vars
wittNeg_zero 📖	mathematical	—	wittNeg MvPolynomial Int.instCommSemiring NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing MvPolynomial.instCommRingMvPolynomial Int.instCommRing MvPolynomial.X	—	MvPolynomial.map_injective Int.cast_injective Rat.instCharZero map_wittStructureInt map_neg RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass MvPolynomial.map_X DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass MvPolynomial.bind₁_X_right xInTermsOfW_zero wittPolynomial_zero MvPolynomial.rename_X
wittOne_pos_eq_zero 📖	mathematical	—	wittOne MvPolynomial Int.instCommSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing MvPolynomial.instCommRingMvPolynomial Int.instCommRing	—	MvPolynomial.map_injective Int.cast_injective Rat.instCharZero map_wittStructureInt map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass map_zero MonoidWithZeroHomClass.toZeroHomClass Nat.strong_induction_on xInTermsOfW_eq Finset.sum_congr map_pow map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass MvPolynomial.bind₁_X_right map_sum MvPolynomial.bind₁_C_right sub_mul one_mul Finset.sum_eq_single 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 invOf_eq_inv pow_zero tsub_zero Nat.instOrderedSub xInTermsOfW_zero one_pow sub_self
wittOne_zero_eq_one 📖	mathematical	—	wittOne MvPolynomial Int.instCommSemiring AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing MvPolynomial.instCommRingMvPolynomial Int.instCommRing	—	MvPolynomial.map_injective Int.cast_injective Rat.instCharZero map_wittStructureInt map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass xInTermsOfW_zero MvPolynomial.bind₁_X_right
wittPow_vars 📖	mathematical	—	Finset Finset.instHasSubset MvPolynomial.vars Int.instCommSemiring wittPow SProd.sprod Finset.instSProd Finset.univ Fin.fintype Finset.range	—	wittStructureInt_vars
wittSub_vars 📖	mathematical	—	Finset Finset.instHasSubset MvPolynomial.vars Int.instCommSemiring wittSub SProd.sprod Finset.instSProd Finset.univ Fin.fintype Finset.range	—	wittStructureInt_vars
wittSub_zero 📖	mathematical	—	wittSub MvPolynomial Int.instCommSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing MvPolynomial.instCommRingMvPolynomial Int.instCommRing MvPolynomial.X	—	MvPolynomial.map_injective Int.cast_injective Rat.instCharZero map_wittStructureInt map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass MvPolynomial.map_X DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass MvPolynomial.bind₁_X_right xInTermsOfW_zero wittPolynomial_zero MvPolynomial.rename_X
wittZSMul_vars 📖	mathematical	—	Finset Finset.instHasSubset MvPolynomial.vars Int.instCommSemiring wittZSMul SProd.sprod Finset.instSProd Finset.univ Fin.fintype Finset.range	—	wittStructureInt_vars
wittZero_eq_zero 📖	mathematical	—	wittZero MvPolynomial Int.instCommSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing MvPolynomial.instCommRingMvPolynomial Int.instCommRing	—	MvPolynomial.map_injective Int.cast_injective Rat.instCharZero map_wittStructureInt map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass MvPolynomial.aeval_zero' constantCoeff_xInTermsOfW
zero_coeff 📖	mathematical	—	coeff WittVector instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	wittZero_eq_zero map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass
zsmul_coeff 📖	mathematical	—	coeff WittVector hasIntScalar peval wittZSMul Matrix.vecCons Matrix.vecEmpty	—	Matrix.cons_val_fin_one Matrix.cons_fin_one

(root)

Definitions

Name	Category	Theorems
WittVector 📖	CompData	183 math math: WittVector.ghostMap.bijective_of_invertible, WittVector.map_id, WittVector.coeff_truncate, WittVector.mapFun.zero, WittVector.mapFun.surjective, WittVector.toZModPow_compat, WittVector.constantCoeff_surjective, WittVector.teichmuller_mul_pow_coeff_of_ne, WittVector.coeff_surjective, WittVector.verschiebung_zmod, WittVector.truncate_comp_lift, WittVector.mapFun.nsmul, WittVector.ghostComponent_apply, WittVector.ghostComponent_verschiebungFun, WittVector.negIsPoly, WittVector.mapFun.add, WittVector.eq_iterate_verschiebung, WittVector.coeff_add_of_disjoint, WittVector.IsocrystalHom.frob_equivariant, WittVector.frobeniusEquiv_symm_apply, TruncatedWittVector.iInf_ker_truncate, WittVector.factorPowSucc_comp_fontaineThetaModPPow, WittVector.zsmul_coeff, WittVector.map_teichmuller, WittVector.verschiebung_coeff_succ, WittVector.init_pow, WittVector.map_coeff, WittVector.pow_coeff, WittVector.mapFun.one, TruncatedWittVector.truncate_wittVector_truncate, WittVector.factorPowSucc_fontaineThetaModPPow_eq, WittVector.truncateFun_one, WittVector.teichmuller_zero, WittVector.iterate_verschiebung_mul, WittVector.verschiebung_nonzero, WittVector.mapFun.sub, WittVector.frobenius_isPoly, WittVector.init_neg, WittVector.mapFun.pow, WittVector.truncate_surjective, WittVector.mk_pow_fontaineTheta, WittVector.truncateFun_surjective, WittVector.verschiebung_injective, WittVector.map_injective, WittVector.coeff_p, WittVector.truncateFun_zero, WittVector.fromPadicInt_comp_toPadicInt, WittVector.frobenius_bijective, WittVector.instNoZeroDivisorsOfCharP, WittVector.frobenius_frobeniusRotation, WittVector.instIsDomain, WittVector.mulN_coeff, WittVector.init_mul, WittVector.sum_coeff_eq_coeff_sum, WittVector.mem_span_p_pow_iff_le_coeff_eq_zero, WittVector.truncateFun_add, WittVector.IsocrystalEquiv.frob_equivariant, WittVector.truncateFun_pow, WittVector.zeroIsPoly, WittVector.pow_dvd_ghostComponent_of_dvd_coeff, WittVector.mapFun.mul, WittVector.init_zsmul, WittVector.idIsPoly, WittVector.mapFun.zsmul, WittVector.mem_ker_truncate, WittVector.fromPadicInt_comp_toPadicInt_ext, WittVector.mulIsPoly₂, TruncatedWittVector.truncate_comp_wittVector_truncate, WittVector.ghostComponent_frobeniusFun, WittVector.init_add, WittVector.matrix_vecEmpty_coeff, WittVector.oneIsPoly, WittVector.exists_eq_pow_p_mul', WittVector.isDiscreteValuationRing, WittVector.iterate_verschiebung_coeff_eq_zero, WittVector.dvd_sub_sum_teichmuller_iterateFrobeniusEquiv_coeff, WittVector.IsPoly.map, WittVector.ker_map_le_ker_mk_comp_ghostComponent, WittVector.fontaineThetaModPPow_teichmuller, WittVector.verschiebung_coeff_zero, WittVector.iterate_frobenius_coeff, TruncatedWittVector.out_injective, WittVector.truncateFun_intCast, WittVector.inv_pair₂, WittVector.irreducible, WittVector.zero_coeff, WittVector.exists_frobenius_solution_fractionRing, WittVector.ghostComponentModPPow_teichmuller_coeff, WittVector.iterate_verschiebung_iterate_frobenius, WittVector.verschiebung_mul_frobenius, WittVector.coeff_frobenius_charP, WittVector.liftEquiv_apply, WittVector.isAdicCompleteIdealSpanP, WittVector.ghostMap_apply, WittVector.inv_pair₁, WittVector.ghostComponent_verschiebung, surjective_fontaineTheta, WittVector.sub_coeff, WittVector.mul_coeff, WittVector.map_verschiebung, WittVector.verschiebung_frobenius, WittVector.one_coeff_zero, WittVector.instLawfulFunctor, WittVector.fontaineTheta_teichmuller, WittVector.truncate_lift, WittVector.ghostComponent_zero_verschiebung, WittVector.coeff_p_pow, WittVector.mul_pow_charP_coeff_zero, WittVector.init_sub, WittVector.StandardOneDimIsocrystal.frobenius_apply, WittVector.one_coeff_eq_of_pos, WittVector.select_add_select_not, WittVector.IsPoly.comp, WittVector.iterate_verschiebung_mul_coeff, WittVector.truncateFun_neg, WittVector.truncateFun_natCast, WittVector.liftEquiv_symm_apply_coe, WittVector.quotientPEquiv_mk, WittVector.toPadicInt_comp_fromPadicInt_ext, WittVector.coeff_p_zero, WittVector.map_eq_zero_iff, WittVector.nth_mul_coeff, WittVector.truncateFun_nsmul, WittVector.toPadicInt_comp_fromPadicInt, WittVector.addIsPoly₂, WittVector.v2_coeff, WittVector.truncateFun_mul, WittVector.verschiebung_shift, WittVector.ghostComponent_frobenius, WittVector.exists_eq_pow_p_mul, WittVector.mapFun.intCast, WittVector.isUnit_of_coeff_zero_ne_zero, WittVector.verschiebung_frobenius_comm, WittVector.quotEquivOfEq_ghostComponentModPPow, WittVector.teichmuller_coeff_zero, WittVector.iterate_verschiebung_mul_left, WittVector.mul_coeff_zero, WittVector.mulN_isPoly, WittVector.iterate_verschiebung_coeff, WittVector.frobeniusEquiv_apply, WittVector.truncate_mk', WittVector.map_surjective, WittVector.neg_coeff, WittVector.IsPoly₂.map, WittVector.instNontrivial, WittVector.verschiebung_coeff_add_one, WittVector.ker_constantCoeff, WittVector.teichmuller_mul_pow_coeff, WittVector.aeval_verschiebungPoly, WittVector.verschiebung_isPoly, WittVector.peval_polyOfInterest', WittVector.constantCoeff_apply, WittVector.nthRemainder_spec, WittVector.coeff_p_pow_eq_zero, WittVector.coe_mkUnit, WittVector.mem_span_p_iff_coeff_zero_eq_zero, WittVector.truncateFun_sub, WittVector.mul_charP_coeff_zero, WittVector.ghostEquiv_coe, WittVector.teichmuller_coeff_pos, WittVector.mk_fontaineTheta, WittVector.add_coeff_zero, WittVector.ghostComponent_zero_verschiebungFun, WittVector.truncateFun_zsmul, WittVector.add_coeff, WittVector.coeff_frobenius, WittVector.mul_pow_charP_coeff_succ, WittVector.frobenius_verschiebung, WittVector.mapFun.natCast, WittVector.mapFun.injective, WittVector.ghostComponent_teichmuller, WittVector.le_coeff_eq_iff_le_sub_coeff_eq_zero, WittVector.init_add_tail, WittVector.truncate_liftFun, WittVector.ghostComponentModPPow_map_mk, WittVector.init_nsmul, WittVector.coeff_p_one, WittVector.nsmul_coeff, WittVector.nth_mul_coeff', WittVector.mapFun.neg, WittVector.peval_polyOfInterest, WittVector.frobenius_zmodp, WittVector.mul_charP_coeff_succ

---

← Back to Index