Documentation Verification Report

Domain

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

Statistics

Metric	Count
Definitions `shift`	1
Theorems `eq_iterate_verschiebung`, `instIsDomain`, `instNoZeroDivisorsOfCharP`, `shift_coeff`, `verschiebung_nonzero`, `verschiebung_shift`	6
Total	7

WittVector

Definitions

Name	Category	Theorems
`shift` 📖	CompOp	3 math math: `eq_iterate_verschiebung`, `shift_coeff`, `verschiebung_shift`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_iterate_verschiebung` 📖	mathematical	`coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`Nat.iterate` `WittVector` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRing` `AddMonoidHom.instFunLike` `verschiebung` `shift`	—	`zero_add` `verschiebung_shift` `LT.lt.trans`
`instIsDomain` 📖	mathematical	—	`IsDomain` `WittVector` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing`	—	`NoZeroDivisors.to_isDomain` `instNontrivial` `IsDomain.toNontrivial` `instNoZeroDivisorsOfCharP` `IsDomain.to_noZeroDivisors`
`instNoZeroDivisorsOfCharP` 📖	mathematical	—	`NoZeroDivisors` `WittVector` `instMul` `instZero`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `verschiebung_nonzero` `iterate_verschiebung_mul_coeff` `zero_coeff` `mul_ne_zero` `pow_ne_zero` `isReduced_of_noZeroDivisors`
`shift_coeff` 📖	mathematical	—	`coeff` `shift`	—	—
`verschiebung_nonzero` 📖	mathematical	—	`Nat.iterate` `WittVector` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRing` `AddMonoidHom.instFunLike` `verschiebung`	—	`ext` `zero_coeff` `Nat.find_spec` `eq_iterate_verschiebung` `Nat.find_min`
`verschiebung_shift` 📖	mathematical	`coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`DFunLike.coe` `AddMonoidHom` `WittVector` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRing` `AddMonoidHom.instFunLike` `verschiebung` `shift`	—	`ext` `verschiebung_coeff_zero` `shift_coeff` `add_comm`

---

← Back to Index