Documentation Verification Report

Complete

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

Statistics

Metric	Count
Definitions `quotientPEquiv`	1
Theorems `eq_zero_of_p_mul_eq_zero`, `isAdicCompleteIdealSpanP`, `ker_constantCoeff`, `le_coeff_eq_iff_le_sub_coeff_eq_zero`, `mem_span_p_iff_coeff_zero_eq_zero`, `mem_span_p_pow_iff_le_coeff_eq_zero`, `quotientPEquiv_mk`	7
Total	8

WittVector

Definitions

Name	Category	Theorems
`quotientPEquiv` 📖	CompOp	1 math math: `quotientPEquiv_mk`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_zero_of_p_mul_eq_zero` 📖	—	`WittVector` `instMul` `instNatCast` `instZero`	—	—	`expChar_prime` `map_eq_zero_iff` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `verschiebung_injective` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Function.Bijective.injective` `frobenius_bijective` `frobenius_verschiebung`
`isAdicCompleteIdealSpanP` 📖	mathematical	—	`IsAdicComplete` `WittVector` `instCommRing` `Ideal.span` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Set` `Set.instSingletonSet` `instNatCast` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule`	—	`expChar_prime` `IsScalarTower.left` `IsScalarTower.right` `ext` `Ideal.mul_top` `Ideal.instIsTwoSided_1` `zero_coeff` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_lt_of_covariant_le` `Nat.instZeroLEOneClass` `Ideal.span_singleton_pow`
`ker_constantCoeff` 📖	mathematical	—	`RingHom.ker` `WittVector` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `RingHom.instFunLike` `RingHom.instRingHomClass` `constantCoeff` `Ideal.span` `Set` `Set.instSingletonSet` `instNatCast`	—	`expChar_prime` `Ideal.ext` `RingHom.instRingHomClass`
`le_coeff_eq_iff_le_sub_coeff_eq_zero` 📖	mathematical	—	`coeff` `WittVector` `instSub` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`TruncatedWittVector.ext` `coeff_truncate` `map_sub` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass`
`mem_span_p_iff_coeff_zero_eq_zero` 📖	mathematical	—	`WittVector` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.span` `Set` `Set.instSingletonSet` `instNatCast` `coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`expChar_prime` `mul_comm` `mul_charP_coeff_zero` `Function.iterate_one` `eq_iterate_verschiebung` `verschiebung_frobenius` `frobeniusEquiv_apply` `RingEquiv.apply_symm_apply`
`mem_span_p_pow_iff_le_coeff_eq_zero` 📖	mathematical	—	`WittVector` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.span` `Set` `Set.instSingletonSet` `hasNatPow` `instNatCast` `coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`expChar_prime` `mul_comm` `mul_pow_charP_coeff_zero` `iterate_verschiebung_iterate_frobenius` `eq_iterate_verschiebung` `Function.Commute.comp_iterate` `Function.Commute.eq_1` `Function.Semiconj.eq_1` `frobeniusEquiv_apply` `RingEquiv.apply_symm_apply` `RingEquiv.symm_apply_apply` `RingEquiv.coe_trans` `RingEquiv.symm_trans_self` `Function.iterate_id`
`quotientPEquiv_mk` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `HasQuotient.Quotient` `WittVector` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `Ideal.instHasQuotient_1` `Ideal.span` `Set` `Set.instSingletonSet` `instNatCast` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ideal.Quotient.commRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `quotientPEquiv` `Submodule.quotientRel` `CommRing.toRing` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `constantCoeff`	—	`expChar_prime`

---

← Back to Index