Documentation Verification Report

Compare

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

Statistics

Metric	Count
Definitions `zmodEquivTrunc`, `equiv`, `fromPadicInt`, `toPadicInt`, `toZModPow`	5
Theorems `card_zmod`, `charP_zmod`, `commutes`, `commutes'`, `commutes_symm`, `commutes_symm'`, `eq_of_le_of_cast_pow_eq_zero`, `zmodEquivTrunc_apply`, `fromPadicInt_comp_toPadicInt`, `fromPadicInt_comp_toPadicInt_ext`, `toPadicInt_comp_fromPadicInt`, `toPadicInt_comp_fromPadicInt_ext`, `toZModPow_compat`, `zmodEquivTrunc_compat`	14
Total	19

TruncatedWittVector

Definitions

Name	Category	Theorems
`zmodEquivTrunc` 📖	CompOp	6 math math: `commutes_symm'`, `zmodEquivTrunc_apply`, `commutes`, `commutes'`, `WittVector.zmodEquivTrunc_compat`, `commutes_symm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_zmod` 📖	mathematical	—	`Fintype.card` `TruncatedWittVector` `ZMod` `instFintype` `ZMod.fintype` `NeZero.of_gt'` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPreorder` `Nat.instCanonicallyOrderedAdd` `Nat.instOne` `Nat.Prime.one_lt'` `Monoid.toNatPow` `Nat.instMonoid`	—	`NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `card` `ZMod.card`
`charP_zmod` 📖	mathematical	—	`CharP` `TruncatedWittVector` `ZMod` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRing` `ZMod.commRing` `Monoid.toNatPow` `Nat.instMonoid`	—	`charP_of_prime_pow_injective` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `card_zmod` `eq_of_le_of_cast_pow_eq_zero` `ZMod.charP`
`commutes` 📖	mathematical	—	`RingHom.comp` `ZMod` `Monoid.toNatPow` `Nat.instMonoid` `TruncatedWittVector` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ZMod.commRing` `instCommRing` `truncate` `RingEquiv.toRingHom` `zmodEquivTrunc` `ZMod.castHom` `pow_dvd_pow` `CommRing.toRing` `ZMod.charP`	—	`RingHom.ext_zmod` `pow_dvd_pow` `ZMod.charP`
`commutes'` 📖	mathematical	—	`DFunLike.coe` `RingHom` `TruncatedWittVector` `ZMod` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `ZMod.commRing` `RingHom.instFunLike` `truncate` `RingEquiv` `Monoid.toNatPow` `Nat.instMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instMul` `Distrib.toAdd` `instAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `zmodEquivTrunc` `Ring.toSemiring` `CommRing.toRing` `ZMod.castHom` `pow_dvd_pow` `ZMod.charP`	—	`pow_dvd_pow` `ZMod.charP` `commutes`
`commutes_symm` 📖	mathematical	—	`RingHom.comp` `TruncatedWittVector` `ZMod` `Monoid.toNatPow` `Nat.instMonoid` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `ZMod.commRing` `RingEquiv.toRingHom` `RingEquiv.symm` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instMul` `Distrib.toAdd` `instAdd` `zmodEquivTrunc` `truncate` `Ring.toSemiring` `CommRing.toRing` `ZMod.castHom` `pow_dvd_pow` `ZMod.charP`	—	`RingHom.ext` `pow_dvd_pow` `ZMod.charP` `commutes_symm'`
`commutes_symm'` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `TruncatedWittVector` `ZMod` `Monoid.toNatPow` `Nat.instMonoid` `instMul` `ZMod.commRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instAdd` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `zmodEquivTrunc` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `RingHom.instFunLike` `truncate` `Ring.toSemiring` `CommRing.toRing` `ZMod.castHom` `pow_dvd_pow` `ZMod.charP`	—	`RingEquiv.injective` `pow_dvd_pow` `ZMod.charP` `commutes'` `RingEquiv.apply_symm_apply`
`eq_of_le_of_cast_pow_eq_zero` 📖	—	`TruncatedWittVector` `hasNatPow` `instNatCast` `instZero`	—	—	`Mathlib.Tactic.Contrapose.contrapose₁` `lt_of_le_of_ne` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `map_natCast` `ext_iff` `WittVector.coeff_truncate` `coeff_zero` `WittVector.coeff_p_pow` `one_ne_zero` `NeZero.one` `CharP.nontrivial_of_char_ne_one` `Nat.Prime.ne_one` `Fact.out`
`zmodEquivTrunc_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `ZMod` `Monoid.toNatPow` `Nat.instMonoid` `TruncatedWittVector` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing` `instMul` `Distrib.toAdd` `instAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `zmodEquivTrunc` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.toSemiring` `CommRing.toRing` `instCommRing` `RingHom.instFunLike` `ZMod.castHom` `charP_zmod`	—	—

WittVector

Definitions

Name	Category	Theorems
`equiv` 📖	CompOp	—
`fromPadicInt` 📖	CompOp	4 math math: `fromPadicInt_comp_toPadicInt`, `fromPadicInt_comp_toPadicInt_ext`, `toPadicInt_comp_fromPadicInt_ext`, `toPadicInt_comp_fromPadicInt`
`toPadicInt` 📖	CompOp	4 math math: `fromPadicInt_comp_toPadicInt`, `fromPadicInt_comp_toPadicInt_ext`, `toPadicInt_comp_fromPadicInt_ext`, `toPadicInt_comp_fromPadicInt`
`toZModPow` 📖	CompOp	1 math math: `toZModPow_compat`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fromPadicInt_comp_toPadicInt` 📖	mathematical	—	`RingHom.comp` `WittVector` `ZMod` `PadicInt` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `ZMod.commRing` `PadicInt.instCommRing` `fromPadicInt` `toPadicInt` `RingHom.id`	—	`hom_ext` `zmodEquivTrunc_compat` `fromPadicInt.eq_1` `RingHom.comp_assoc` `truncate_comp_lift` `PadicInt.lift_spec` `toZModPow_compat` `RingEquiv.toRingHom_comp_symm_toRingHom` `RingHom.id_comp` `RingHom.comp_id`
`fromPadicInt_comp_toPadicInt_ext` 📖	mathematical	—	`DFunLike.coe` `RingHom` `WittVector` `ZMod` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `ZMod.commRing` `RingHom.instFunLike` `RingHom.comp` `PadicInt` `PadicInt.instCommRing` `fromPadicInt` `toPadicInt` `RingHom.id`	—	`fromPadicInt_comp_toPadicInt`
`toPadicInt_comp_fromPadicInt` 📖	mathematical	—	`RingHom.comp` `PadicInt` `WittVector` `ZMod` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `PadicInt.instCommRing` `instCommRing` `ZMod.commRing` `toPadicInt` `fromPadicInt` `RingHom.id`	—	`PadicInt.toZModPow_eq_iff_ext` `RingHom.comp_assoc` `toZModPow_compat` `toPadicInt.eq_1` `PadicInt.lift_spec` `zmodEquivTrunc_compat` `RingHom.comp_id` `truncate_comp_lift` `RingEquiv.symm_toRingHom_comp_toRingHom` `RingHom.id_comp`
`toPadicInt_comp_fromPadicInt_ext` 📖	mathematical	—	`DFunLike.coe` `RingHom` `PadicInt` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `PadicInt.instCommRing` `RingHom.instFunLike` `RingHom.comp` `WittVector` `ZMod` `instCommRing` `ZMod.commRing` `toPadicInt` `fromPadicInt` `RingHom.id`	—	`toPadicInt_comp_fromPadicInt`
`toZModPow_compat` 📖	mathematical	—	`RingHom.comp` `WittVector` `ZMod` `Monoid.toNatPow` `Nat.instMonoid` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `ZMod.commRing` `Ring.toSemiring` `CommRing.toRing` `ZMod.castHom` `pow_dvd_pow` `ZMod.charP` `toZModPow`	—	`pow_dvd_pow` `ZMod.charP` `TruncatedWittVector.commutes_symm` `RingHom.comp_assoc` `TruncatedWittVector.truncate_comp_wittVector_truncate`
`zmodEquivTrunc_compat` 📖	mathematical	—	`RingHom.comp` `PadicInt` `TruncatedWittVector` `ZMod` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `PadicInt.instCommRing` `TruncatedWittVector.instCommRing` `ZMod.commRing` `TruncatedWittVector.truncate` `Monoid.toNatPow` `Nat.instMonoid` `RingEquiv.toRingHom` `TruncatedWittVector.zmodEquivTrunc` `PadicInt.toZModPow`	—	`RingHom.comp_assoc` `pow_dvd_pow` `ZMod.charP` `TruncatedWittVector.commutes` `PadicInt.zmod_cast_comp_toZModPow`

---

← Back to Index