IsPoly

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

Statistics

Metric	Count
Definitions IsPoly, IsPoly, instInhabitedId, IsPoly₂, instInhabitedHAdd, ghostCalc, ghostSimp, onePoly	8
Theorems comp, comp₂, ext, map, poly, comp, diag, ext, map, poly, addIsPoly₂, bind₁_onePoly_wittPolynomial, bind₁_zero_wittPolynomial, idIsPoly, idIsPolyI', mulIsPoly₂, negIsPoly, oneIsPoly, poly_eq_of_wittPolynomial_bind_eq, poly_eq_of_wittPolynomial_bind_eq', zeroIsPoly	21
Total	29

WittVector

Definitions

Name	Category	Theorems
IsPoly 📖	CompData	14 math math: negIsPoly, idIsPolyI', frobenius_isPoly, zeroIsPoly, idIsPoly, oneIsPoly, IsPoly₂.diag, select_isPoly, frobeniusFun_isPoly, IsPoly.comp, init_isPoly, mulN_isPoly, verschiebung_isPoly, verschiebungFun_isPoly
IsPoly₂ 📖	CompData	4 math math: mulIsPoly₂, IsPoly₂.comp, addIsPoly₂, IsPoly.comp₂
onePoly 📖	CompOp	1 math math: bind₁_onePoly_wittPolynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addIsPoly₂ 📖	mathematical	—	IsPoly₂ WittVector instAdd	—	add_coeff
bind₁_onePoly_wittPolynomial 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial Int.instCommSemiring CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id AlgHom.funLike MvPolynomial.bind₁ onePoly wittPolynomial Int.instCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing MvPolynomial.instCommRingMvPolynomial	—	wittPolynomial_eq_sum_C_mul_X_pow map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass Finset.sum_eq_single map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHomClass.toRingHomClass MvPolynomial.bind₁_X_right 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 IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Nat.instNoMaxOrder pow_zero eq_intCast Int.cast_one tsub_zero Nat.instOrderedSub one_mul MvPolynomial.instIsReduced Int.instIsStrictOrderedRing AddGroup.existsAddOfLE MvPolynomial.nontrivial_of_nontrivial Int.instNontrivial instIsEmptyFalse one_pow
bind₁_zero_wittPolynomial 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommRing.toCommSemiring CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id AlgHom.funLike MvPolynomial.bind₁ Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing MvPolynomial.instCommRingMvPolynomial wittPolynomial	—	MvPolynomial.aeval_eq_bind₁ MvPolynomial.aeval_zero constantCoeff_wittPolynomial map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
idIsPoly 📖	mathematical	—	IsPoly WittVector	—	MvPolynomial.aeval_X
idIsPolyI' 📖	mathematical	—	IsPoly	—	idIsPoly
mulIsPoly₂ 📖	mathematical	—	IsPoly₂ WittVector instMul	—	mul_coeff
negIsPoly 📖	mathematical	—	IsPoly WittVector instNeg	—	neg_coeff MvPolynomial.aeval_eq_eval₂Hom MvPolynomial.eval₂Hom_rename MvPolynomial.eval₂Hom_congr Fintype.complete
oneIsPoly 📖	mathematical	—	IsPoly WittVector instOne	—	one_coeff_zero map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass one_coeff_eq_of_pos map_zero MonoidWithZeroHomClass.toZeroHomClass
poly_eq_of_wittPolynomial_bind_eq 📖	—	DFunLike.coe AlgHom MvPolynomial Int.instCommSemiring CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id AlgHom.funLike MvPolynomial.bind₁ wittPolynomial Int.instCommRing	—	—	MvPolynomial.map_injective Int.cast_injective Rat.instCharZero NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' MvPolynomial.map_bind₁ map_wittPolynomial bind₁_wittPolynomial_xInTermsOfW MvPolynomial.bind₁_X_right
poly_eq_of_wittPolynomial_bind_eq' 📖	—	DFunLike.coe AlgHom MvPolynomial Int.instCommSemiring CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id AlgHom.funLike MvPolynomial.bind₁ wittPolynomial Int.instCommRing	—	—	MvPolynomial.map_injective Int.cast_injective Rat.instCharZero NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' MvPolynomial.map_bind₁ map_wittPolynomial bind₁_wittPolynomial_xInTermsOfW MvPolynomial.bind₁_X_right
zeroIsPoly 📖	mathematical	—	IsPoly WittVector instZero	—	zero_coeff map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass

WittVector.IsPoly

Definitions

Name	Category	Theorems
instInhabitedId 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	—	WittVector.IsPoly WittVector	—	MvPolynomial.aeval_bind₁
comp₂ 📖	mathematical	—	WittVector.IsPoly₂	—	MvPolynomial.aeval_bind₁
ext 📖	—	DFunLike.coe RingHom WittVector Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring WittVector.instCommRing RingHom.instFunLike WittVector.ghostComponent	—	—	WittVector.ext WittVector.poly_eq_of_wittPolynomial_bind_eq MvPolynomial.funext Int.instIsDomain Int.infinite MvPolynomial.hom_bind₁ RingEquiv.injective RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass MvPolynomial.map_eval₂Hom MvPolynomial.eval₂Hom_congr RingHom.ext_int
map 📖	mathematical	—	DFunLike.coe RingHom WittVector Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring WittVector.instCommRing RingHom.instFunLike WittVector.map	—	WittVector.ext MvPolynomial.map_aeval WittVector.map_coeff RingHom.ext_int
poly 📖	mathematical	—	WittVector.coeff DFunLike.coe AlgHom MvPolynomial Int.instCommSemiring CommSemiring.toSemiring MvPolynomial.commSemiring CommRing.toCommSemiring MvPolynomial.algebra Algebra.id Ring.toIntAlgebra CommRing.toRing AlgHom.funLike MvPolynomial.aeval	—	—

WittVector.IsPoly₂

Definitions

Name	Category	Theorems
instInhabitedHAdd 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	—	WittVector.IsPoly₂	—	MvPolynomial.aeval_bind₁ MvPolynomial.eval₂Hom_congr Fintype.complete Matrix.cons_val' Matrix.cons_val_fin_one MvPolynomial.eval₂Hom_rename
diag 📖	mathematical	—	WittVector.IsPoly	—	MvPolynomial.aeval_bind₁ MvPolynomial.eval₂Hom_congr Fintype.complete Matrix.cons_val' Matrix.cons_val_fin_one MvPolynomial.aeval_X
ext 📖	—	DFunLike.coe RingHom WittVector Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring WittVector.instCommRing RingHom.instFunLike WittVector.ghostComponent	—	—	WittVector.ext WittVector.poly_eq_of_wittPolynomial_bind_eq' MvPolynomial.funext Int.instIsDomain Int.infinite MvPolynomial.hom_bind₁ RingEquiv.injective RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass MvPolynomial.map_eval₂Hom MvPolynomial.eval₂Hom_congr RingHom.ext_int ULift.ext Fintype.complete
map 📖	mathematical	—	DFunLike.coe RingHom WittVector Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring WittVector.instCommRing RingHom.instFunLike WittVector.map	—	WittVector.ext MvPolynomial.map_aeval MvPolynomial.eval₂Hom_congr RingHom.ext_int Fintype.complete Matrix.cons_val' Matrix.cons_val_fin_one
poly 📖	mathematical	—	WittVector.coeff WittVector.peval Matrix.vecCons Matrix.vecEmpty	—	—

WittVector.Tactic

Definitions

Name	Category	Theorems
ghostCalc 📖	CompOp	—
ghostSimp 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
IsPoly 📖	CompData	1 math math: Poly.isPoly

---

← Back to Index