Documentation Verification Report

InitTail

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

Statistics

Metric	Count
Definitions `init`, `initRing`, `select`, `selectPoly`, `tail`	5
Theorems `coeff_add_of_disjoint`, `coeff_select`, `init_add`, `init_add_tail`, `init_init`, `init_isPoly`, `init_mul`, `init_neg`, `init_nsmul`, `init_pow`, `init_sub`, `init_zsmul`, `select_add_select_not`, `select_isPoly`	14
Total	19

WittVector

Definitions

Name	Category	Theorems
`init` 📖	CompOp	11 math math: `init_pow`, `init_neg`, `init_mul`, `init_zsmul`, `init_add`, `init_sub`, `init_isPoly`, `init_init`, `out_truncateFun`, `init_add_tail`, `init_nsmul`
`initRing` 📖	CompOp	—
`select` 📖	CompOp	3 math math: `select_isPoly`, `select_add_select_not`, `coeff_select`
`selectPoly` 📖	CompOp	1 math math: `coeff_select`
`tail` 📖	CompOp	1 math math: `init_add_tail`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeff_add_of_disjoint` 📖	mathematical	`coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`WittVector` `instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib`	—	`ext` `select.eq_1` `select_add_select_not` `add_zero` `zero_add`
`coeff_select` 📖	mathematical	—	`coeff` `select` `DFunLike.coe` `AlgHom` `MvPolynomial` `Int.instCommSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `CommRing.toCommSemiring` `MvPolynomial.algebra` `Algebra.id` `Ring.toIntAlgebra` `CommRing.toRing` `AlgHom.funLike` `MvPolynomial.aeval` `selectPoly`	—	`MvPolynomial.aeval_X` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass`
`init_add` 📖	mathematical	—	`init` `WittVector` `instAdd`	—	`ext_iff` `add_coeff` `MvPolynomial.eval₂Hom_congr'` `RingHom.ext_int` `wittAdd_vars` `Fintype.complete` `Matrix.cons_val'` `Matrix.empty_val'` `Matrix.cons_val_fin_one`
`init_add_tail` 📖	mathematical	—	`WittVector` `instAdd` `init` `tail`	—	`select_add_select_not`
`init_init` 📖	mathematical	—	`init`	—	`ext_iff`
`init_isPoly` 📖	mathematical	—	`IsPoly` `init`	—	`select_isPoly`
`init_mul` 📖	mathematical	—	`init` `WittVector` `instMul`	—	`ext_iff` `mul_coeff` `MvPolynomial.eval₂Hom_congr'` `RingHom.ext_int` `wittMul_vars` `Fintype.complete` `Matrix.cons_val'` `Matrix.empty_val'` `Matrix.cons_val_fin_one`
`init_neg` 📖	mathematical	—	`init` `WittVector` `instNeg`	—	`ext_iff` `neg_coeff` `MvPolynomial.eval₂Hom_congr'` `RingHom.ext_int` `wittNeg_vars` `Fintype.complete` `Matrix.cons_val'` `Matrix.empty_val'` `Matrix.cons_val_fin_one`
`init_nsmul` 📖	mathematical	—	`init` `WittVector` `hasNatScalar`	—	`ext_iff` `nsmul_coeff` `MvPolynomial.eval₂Hom_congr'` `RingHom.ext_int` `wittNSMul_vars` `Fintype.complete` `Matrix.cons_val'` `Matrix.empty_val'` `Matrix.cons_val_fin_one`
`init_pow` 📖	mathematical	—	`init` `WittVector` `hasNatPow`	—	`ext_iff` `pow_coeff` `MvPolynomial.eval₂Hom_congr'` `RingHom.ext_int` `wittPow_vars` `Fintype.complete` `Matrix.cons_val'` `Matrix.empty_val'` `Matrix.cons_val_fin_one`
`init_sub` 📖	mathematical	—	`init` `WittVector` `instSub`	—	`ext_iff` `sub_coeff` `MvPolynomial.eval₂Hom_congr'` `RingHom.ext_int` `wittSub_vars` `Fintype.complete` `Matrix.cons_val'` `Matrix.empty_val'` `Matrix.cons_val_fin_one`
`init_zsmul` 📖	mathematical	—	`init` `WittVector` `hasIntScalar`	—	`ext_iff` `zsmul_coeff` `MvPolynomial.eval₂Hom_congr'` `RingHom.ext_int` `wittZSMul_vars` `Fintype.complete` `Matrix.cons_val'` `Matrix.empty_val'` `Matrix.cons_val_fin_one`
`select_add_select_not` 📖	mathematical	—	`WittVector` `instAdd` `select`	—	`IsPoly₂.diag` `IsPoly₂.comp` `addIsPoly₂` `select_isPoly` `IsPoly.ext` `idIsPolyI'` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `wittPolynomial_eq_sum_C_mul_X_pow` `Finset.sum_congr` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHomClass.toRingHomClass` `MvPolynomial.bind₁_C_right` `MvPolynomial.bind₁_X_right` `Distrib.leftDistribClass` `mul_eq_mul_left_iff` `IsCancelMulZero.toIsLeftCancelMulZero` `MvPolynomial.instIsCancelMulZeroOfIsCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `Int.instIsCancelMulZero` `ite_pow` `zero_pow` `pow_ne_zero` `isReduced_of_noZeroDivisors` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.ne_zero` `Fact.out` `LT.lt.ne'` `NeZero.of_gt'` `Nat.Prime.one_lt'` `add_zero` `zero_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `MvPolynomial.aeval_bind₁`
`select_isPoly` 📖	mathematical	—	`IsPoly` `select`	—	`coeff_select`

---

← Back to Index