Documentation Verification Report

Verschiebung

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

Statistics

Metric	Count
Definitions `verschiebung`, `verschiebungFun`, `verschiebungPoly`	3
Theorems `aeval_verschiebungPoly`, `aeval_verschiebung_poly'`, `bind₁_verschiebungPoly_wittPolynomial`, `ghostComponent_verschiebung`, `ghostComponent_verschiebungFun`, `ghostComponent_zero_verschiebung`, `ghostComponent_zero_verschiebungFun`, `map_verschiebung`, `verschiebungFun_coeff`, `verschiebungFun_coeff_succ`, `verschiebungFun_coeff_zero`, `verschiebungFun_isPoly`, `verschiebungPoly_zero`, `verschiebung_coeff_add_one`, `verschiebung_coeff_succ`, `verschiebung_coeff_zero`, `verschiebung_injective`, `verschiebung_isPoly`	18
Total	21

WittVector

Definitions

Name	Category	Theorems
`verschiebung` 📖	CompOp	23 math math: `verschiebung_zmod`, `eq_iterate_verschiebung`, `verschiebung_coeff_succ`, `iterate_verschiebung_mul`, `verschiebung_nonzero`, `verschiebung_injective`, `iterate_verschiebung_coeff_eq_zero`, `verschiebung_coeff_zero`, `iterate_verschiebung_iterate_frobenius`, `verschiebung_mul_frobenius`, `ghostComponent_verschiebung`, `map_verschiebung`, `verschiebung_frobenius`, `ghostComponent_zero_verschiebung`, `iterate_verschiebung_mul_coeff`, `verschiebung_shift`, `verschiebung_frobenius_comm`, `iterate_verschiebung_mul_left`, `iterate_verschiebung_coeff`, `verschiebung_coeff_add_one`, `aeval_verschiebungPoly`, `verschiebung_isPoly`, `frobenius_verschiebung`
`verschiebungFun` 📖	CompOp	7 math math: `aeval_verschiebung_poly'`, `ghostComponent_verschiebungFun`, `verschiebungFun_coeff`, `verschiebungFun_coeff_zero`, `verschiebungFun_coeff_succ`, `ghostComponent_zero_verschiebungFun`, `verschiebungFun_isPoly`
`verschiebungPoly` 📖	CompOp	4 math math: `aeval_verschiebung_poly'`, `bind₁_verschiebungPoly_wittPolynomial`, `aeval_verschiebungPoly`, `verschiebungPoly_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aeval_verschiebungPoly` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPolynomial` `Int.instCommSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `CommRing.toCommSemiring` `MvPolynomial.algebra` `Algebra.id` `Ring.toIntAlgebra` `CommRing.toRing` `AlgHom.funLike` `MvPolynomial.aeval` `coeff` `verschiebungPoly` `AddMonoidHom` `WittVector` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instCommRing` `AddMonoidHom.instFunLike` `verschiebung`	—	`aeval_verschiebung_poly'`
`aeval_verschiebung_poly'` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPolynomial` `Int.instCommSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `CommRing.toCommSemiring` `MvPolynomial.algebra` `Algebra.id` `Ring.toIntAlgebra` `CommRing.toRing` `AlgHom.funLike` `MvPolynomial.aeval` `coeff` `verschiebungPoly` `verschiebungFun`	—	`map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `verschiebungFun_coeff_zero` `verschiebungPoly.eq_1` `verschiebungFun_coeff_succ` `MvPolynomial.aeval_X` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`bind₁_verschiebungPoly_wittPolynomial` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPolynomial` `Int.instCommSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id` `AlgHom.funLike` `MvPolynomial.bind₁` `verschiebungPoly` `wittPolynomial` `Int.instCommRing` `CommRing.toCommSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MvPolynomial.instCommRingMvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`MvPolynomial.funext` `Int.instIsDomain` `Int.infinite` `wittPolynomial_zero` `MvPolynomial.bind₁_X_right` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `map_natCast` `MvPolynomial.hom_bind₁` `MvPolynomial.eval₂Hom_congr` `RingHom.ext_int` `ghostComponent_verschiebung`
`ghostComponent_verschiebung` 📖	mathematical	—	`DFunLike.coe` `RingHom` `WittVector` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `RingHom.instFunLike` `ghostComponent` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddMonoidHom.instFunLike` `verschiebung` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toNatCast`	—	`ghostComponent_verschiebungFun`
`ghostComponent_verschiebungFun` 📖	mathematical	—	`DFunLike.coe` `RingHom` `WittVector` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `RingHom.instFunLike` `ghostComponent` `verschiebungFun` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`aeval_wittPolynomial` `Finset.sum_range_succ'` `verschiebungFun_coeff` `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` `add_zero` `Finset.mul_sum` `Finset.sum_congr` `pow_succ'` `mul_assoc`
`ghostComponent_zero_verschiebung` 📖	mathematical	—	`DFunLike.coe` `RingHom` `WittVector` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `RingHom.instFunLike` `ghostComponent` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddMonoidHom.instFunLike` `verschiebung` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`ghostComponent_zero_verschiebungFun`
`ghostComponent_zero_verschiebungFun` 📖	mathematical	—	`DFunLike.coe` `RingHom` `WittVector` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `RingHom.instFunLike` `ghostComponent` `verschiebungFun` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`ghostComponent_apply` `aeval_wittPolynomial` `Finset.range_one` `Finset.sum_singleton` `verschiebungFun_coeff_zero` `pow_zero` `pow_one` `one_mul`
`map_verschiebung` 📖	mathematical	—	`DFunLike.coe` `RingHom` `WittVector` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `RingHom.instFunLike` `map` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddMonoidHom.instFunLike` `verschiebung`	—	`ext` `RingHom.map_zero`
`verschiebungFun_coeff` 📖	mathematical	—	`coeff` `verschiebungFun` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	—
`verschiebungFun_coeff_succ` 📖	mathematical	—	`coeff` `verschiebungFun`	—	—
`verschiebungFun_coeff_zero` 📖	mathematical	—	`coeff` `verschiebungFun` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`verschiebungFun_coeff`
`verschiebungFun_isPoly` 📖	mathematical	—	`IsPoly` `verschiebungFun`	—	`aeval_verschiebung_poly'`
`verschiebungPoly_zero` 📖	mathematical	—	`verschiebungPoly` `MvPolynomial` `Int.instCommSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MvPolynomial.instCommRingMvPolynomial` `Int.instCommRing`	—	—
`verschiebung_coeff_add_one` 📖	mathematical	—	`coeff` `DFunLike.coe` `AddMonoidHom` `WittVector` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRing` `AddMonoidHom.instFunLike` `verschiebung`	—	—
`verschiebung_coeff_succ` 📖	mathematical	—	`coeff` `DFunLike.coe` `AddMonoidHom` `WittVector` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRing` `AddMonoidHom.instFunLike` `verschiebung`	—	—
`verschiebung_coeff_zero` 📖	mathematical	—	`coeff` `DFunLike.coe` `AddMonoidHom` `WittVector` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRing` `AddMonoidHom.instFunLike` `verschiebung` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	—
`verschiebung_injective` 📖	mathematical	—	`WittVector` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRing` `AddMonoidHom.instFunLike` `verschiebung`	—	`injective_iff_map_eq_zero` `AddMonoidHom.instAddMonoidHomClass` `ext` `verschiebung_coeff_succ` `zero_coeff`
`verschiebung_isPoly` 📖	mathematical	—	`IsPoly` `DFunLike.coe` `AddMonoidHom` `WittVector` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRing` `AddMonoidHom.instFunLike` `verschiebung`	—	`verschiebungFun_isPoly`

---

← Back to Index