Identities

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

Statistics

Metric	Count
Definitions	0
Theorems `p_nonzero`, `coeff_p`, `coeff_p_one`, `coeff_p_pow`, `coeff_p_pow_eq_zero`, `coeff_p_zero`, `frobenius_verschiebung`, `iterate_frobenius_coeff`, `iterate_verschiebung_coeff`, `iterate_verschiebung_coeff_eq_zero`, `iterate_verschiebung_iterate_frobenius`, `iterate_verschiebung_mul`, `iterate_verschiebung_mul_coeff`, `iterate_verschiebung_mul_left`, `mul_charP_coeff_succ`, `mul_charP_coeff_zero`, `mul_pow_charP_coeff_succ`, `mul_pow_charP_coeff_zero`, `p_nonzero`, `verschiebung_frobenius`, `verschiebung_frobenius_comm`, `verschiebung_mul_frobenius`, `verschiebung_zmod`	23
Total	23

WittVector

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeff_p` 📖	mathematical	—	`coeff` `WittVector` `instNatCast` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`pow_one` `coeff_p_pow` `coeff_p_pow_eq_zero`
`coeff_p_one` 📖	mathematical	—	`coeff` `WittVector` `instNatCast` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`coeff_p`
`coeff_p_pow` 📖	mathematical	—	`coeff` `WittVector` `hasNatPow` `instNatCast` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`pow_zero` `one_coeff_zero` `pow_succ` `frobenius_verschiebung` `coeff_frobenius_charP` `verschiebung_coeff_succ` `one_pow`
`coeff_p_pow_eq_zero` 📖	mathematical	—	`coeff` `WittVector` `hasNatPow` `instNatCast` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`pow_zero` `one_coeff_eq_of_pos` `pow_succ` `frobenius_verschiebung` `coeff_frobenius_charP` `verschiebung_coeff_zero` `zero_pow` `Nat.Prime.ne_zero` `Fact.out` `verschiebung_coeff_succ`
`coeff_p_zero` 📖	mathematical	—	`coeff` `WittVector` `instNatCast` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`coeff_p` `zero_ne_one`
`frobenius_verschiebung` 📖	mathematical	—	`DFunLike.coe` `RingHom` `WittVector` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `RingHom.instFunLike` `frobenius` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddMonoidHom.instFunLike` `verschiebung` `instMul` `instNatCast`	—	`IsPoly.comp` `frobenius_isPoly` `verschiebung_isPoly` `mulN_isPoly` `IsPoly.ext` `ghostComponent_frobenius` `ghostComponent_verschiebung` `RingHom.map_mul` `map_natCast` `RingHom.instRingHomClass` `mul_comm`
`iterate_frobenius_coeff` 📖	mathematical	—	`coeff` `Nat.iterate` `WittVector` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `RingHom.instFunLike` `frobenius` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Nat.instMonoid`	—	`pow_zero` `pow_one` `Function.iterate_succ_apply'` `coeff_frobenius_charP` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.RingNF.nat_rawCast_1` `mul_one` `add_zero` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.pow_one_cast`
`iterate_verschiebung_coeff` 📖	mathematical	—	`coeff` `Nat.iterate` `WittVector` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRing` `AddMonoidHom.instFunLike` `verschiebung`	—	`add_zero` `Function.iterate_succ_apply'` `verschiebung_coeff_succ`
`iterate_verschiebung_coeff_eq_zero` 📖	mathematical	—	`coeff` `Nat.iterate` `WittVector` `DFunLike.coe` `AddMonoidHom` `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`	—	`Function.iterate_succ_apply'` `verschiebung_coeff_zero` `verschiebung_coeff_succ` `Nat.instNoMaxOrder`
`iterate_verschiebung_iterate_frobenius` 📖	mathematical	—	`Nat.iterate` `WittVector` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRing` `AddMonoidHom.instFunLike` `verschiebung` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `frobenius` `instMul` `hasNatPow` `instNatCast`	—	`Function.Commute.comp_iterate` `verschiebung_frobenius_comm` `pow_zero` `mul_one` `Function.iterate_succ_apply'` `pow_succ` `verschiebung_frobenius` `mul_assoc`
`iterate_verschiebung_mul` 📖	mathematical	—	`WittVector` `instMul` `Nat.iterate` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRing` `AddMonoidHom.instFunLike` `verschiebung` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `frobenius`	—	`iterate_verschiebung_mul_left` `Function.Commute.iterate_iterate` `verschiebung_frobenius_comm` `mul_comm` `Function.iterate_add_apply`
`iterate_verschiebung_mul_coeff` 📖	mathematical	—	`coeff` `WittVector` `instMul` `Nat.iterate` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRing` `AddMonoidHom.instFunLike` `verschiebung` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Nat.instMonoid`	—	`iterate_verschiebung_mul` `zero_add` `iterate_verschiebung_coeff` `mul_coeff_zero` `iterate_frobenius_coeff`
`iterate_verschiebung_mul_left` 📖	mathematical	—	`WittVector` `instMul` `Nat.iterate` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRing` `AddMonoidHom.instFunLike` `verschiebung` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `frobenius`	—	`Function.iterate_succ_apply'` `verschiebung_mul_frobenius` `Function.iterate_succ_apply`
`mul_charP_coeff_succ` 📖	mathematical	—	`coeff` `WittVector` `instMul` `instNatCast` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`frobenius_verschiebung` `coeff_frobenius_charP` `verschiebung_coeff_succ`
`mul_charP_coeff_zero` 📖	mathematical	—	`coeff` `WittVector` `instMul` `instNatCast` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`frobenius_verschiebung` `coeff_frobenius_charP` `verschiebung_coeff_zero` `zero_pow` `Nat.Prime.ne_zero` `Fact.out`
`mul_pow_charP_coeff_succ` 📖	mathematical	—	`coeff` `WittVector` `instMul` `hasNatPow` `instNatCast` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Nat.instMonoid`	—	`pow_zero` `mul_one` `add_zero` `pow_one` `pow_succ` `mul_assoc` `add_assoc` `mul_charP_coeff_succ` `pow_mul`
`mul_pow_charP_coeff_zero` 📖	mathematical	—	`coeff` `WittVector` `instMul` `hasNatPow` `instNatCast` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`pow_succ` `mul_assoc` `mul_charP_coeff_zero` `mul_charP_coeff_succ` `Nat.instNoMaxOrder` `zero_pow` `Nat.Prime.ne_zero` `Fact.out`
`p_nonzero` 📖	—	—	—	—	`zero_coeff` `NeZero.one` `coeff_p_one`
`verschiebung_frobenius` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `WittVector` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRing` `AddMonoidHom.instFunLike` `verschiebung` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `frobenius` `instMul` `instNatCast`	—	`ext` `mul_charP_coeff_zero` `verschiebung_coeff_zero` `mul_charP_coeff_succ` `verschiebung_coeff_succ` `coeff_frobenius_charP`
`verschiebung_frobenius_comm` 📖	mathematical	—	`Function.Commute` `WittVector` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRing` `AddMonoidHom.instFunLike` `verschiebung` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `frobenius`	—	`verschiebung_frobenius` `frobenius_verschiebung`
`verschiebung_mul_frobenius` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `WittVector` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRing` `AddMonoidHom.instFunLike` `verschiebung` `instMul` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `frobenius`	—	`IsPoly.comp₂` `verschiebung_isPoly` `IsPoly₂.comp` `mulIsPoly₂` `idIsPolyI'` `frobenius_isPoly` `IsPoly₂.ext` `ghostComponent_zero_verschiebung` `RingHom.map_mul` `MulZeroClass.zero_mul` `ghostComponent_verschiebung` `ghostComponent_frobenius` `mul_assoc`
`verschiebung_zmod` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `WittVector` `ZMod` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRing` `ZMod.commRing` `AddMonoidHom.instFunLike` `verschiebung` `instMul` `instNatCast`	—	`frobenius_verschiebung` `frobenius_zmodp`

WittVector.FractionRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`p_nonzero` 📖	—	—	—	—	`map_natCast` `RingHom.instRingHomClass` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `IsFractionRing.injective` `Localization.isLocalization` `WittVector.p_nonzero`

---

← Back to Index