MulP

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

Statistics

Metric	Count
Definitions wittMulN	1
Theorems bind₁_wittMulN_wittPolynomial, mulN_coeff, mulN_isPoly	3
Total	4

WittVector

Definitions

Name	Category	Theorems
wittMulN 📖	CompOp	2 math math: mulN_coeff, bind₁_wittMulN_wittPolynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bind₁_wittMulN_wittPolynomial 📖	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₁ wittMulN wittPolynomial Int.instCommRing CommRing.toCommSemiring AddMonoidAlgebra.instMul Finsupp.instAdd AddMonoid.toAddZeroClass AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne AddMonoidAlgebra.ring Int.instRing	—	bind₁_zero_wittPolynomial CharP.cast_eq_zero MvPolynomial.instCharP CharP.ofCharZero Int.instCharZero MulZeroClass.zero_mul wittMulN.eq_2 MvPolynomial.bind₁_bind₁ wittAdd.eq_1 wittStructureInt_prop map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass MvPolynomial.bind₁_X_right Nat.cast_succ add_mul Distrib.rightDistribClass one_mul MvPolynomial.bind₁_rename MvPolynomial.bind₁_X_left
mulN_coeff 📖	mathematical	—	coeff WittVector instMul instNatCast DFunLike.coe AlgHom MvPolynomial Int.instCommSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid CommRing.toCommSemiring AddMonoidAlgebra.algebra Algebra.id Ring.toIntAlgebra CommRing.toRing AlgHom.funLike MvPolynomial.aeval wittMulN	—	Nat.cast_zero MulZeroClass.mul_zero zero_coeff map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass wittMulN.eq_2 Nat.cast_add Nat.cast_one mul_add Distrib.leftDistribClass mul_one MvPolynomial.aeval_bind₁ add_coeff MvPolynomial.eval₂Hom_congr RingHom.ext_int Fintype.complete Matrix.cons_val' Matrix.cons_val_fin_one MvPolynomial.aeval_X
mulN_isPoly 📖	mathematical	—	IsPoly WittVector instMul instNatCast	—	mulN_coeff

---

← Back to Index