Documentation Verification Report

DiscreteValuationRing

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

Statistics

Metric	Count
Definitions `inverseCoeff`, `mkUnit`, `succNthValUnits`	3
Theorems `coe_mkUnit`, `exists_eq_pow_p_mul`, `exists_eq_pow_p_mul'`, `irreducible`, `isDiscreteValuationRing`, `isUnit_of_coeff_zero_ne_zero`	6
Total	9

WittVector

Definitions

Name	Category	Theorems
`inverseCoeff` 📖	CompOp	—
`mkUnit` 📖	CompOp	1 math math: `coe_mkUnit`
`succNthValUnits` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_mkUnit` 📖	mathematical	`coeff` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`WittVector` `instCommRing` `mkUnit`	—	—
`exists_eq_pow_p_mul` 📖	mathematical	—	`WittVector` `instMul` `hasNatPow` `instNatCast`	—	`expChar_prime` `verschiebung_nonzero` `Function.Surjective.iterate` `Function.Bijective.surjective` `frobenius_bijective` `Function.Commute.comp_iterate` `verschiebung_frobenius_comm` `Mathlib.Tactic.Contrapose.contrapose₄` `zero_pow` `pow_ne_zero` `isReduced_of_noZeroDivisors` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.ne_zero` `Fact.out` `iterate_frobenius_coeff` `mul_left_iterate` `mul_comm` `verschiebung_frobenius`
`exists_eq_pow_p_mul'` 📖	mathematical	—	`WittVector` `instMul` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `hasNatPow` `instNatCast` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing`	—	`expChar_prime` `exists_eq_pow_p_mul`
`irreducible` 📖	mathematical	—	`Irreducible` `WittVector` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instNatCast`	—	`coeff_p_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `RingHom.isUnit_map` `mul_ne_zero_iff` `instNoZeroDivisorsOfCharP` `IsDomain.to_noZeroDivisors` `instIsDomain` `p_nonzero` `verschiebung_nonzero` `isUnit_of_coeff_zero_ne_zero` `one_ne_zero` `NeZero.one` `coeff_p_one` `add_comm` `Function.iterate_succ'` `iterate_verschiebung_mul`
`isDiscreteValuationRing` 📖	mathematical	—	`IsDiscreteValuationRing` `WittVector` `instCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instIsDomain` `instIsDomain` `Field.toSemifield`	—	`expChar_prime` `IsDiscreteValuationRing.ofHasUnitMulPowIrreducibleFactorization` `instIsDomain` `instIsDomain` `irreducible` `exists_eq_pow_p_mul'`
`isUnit_of_coeff_zero_ne_zero` 📖	mathematical	—	`IsUnit` `WittVector` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`Units.isUnit`

---

← Back to Index