Documentation Verification Report

Frobenius

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

Statistics

Metric	Count
Definitions `frobenius`, `frobeniusEquiv`, `frobeniusFun`, `frobeniusPoly`, `frobeniusPolyAux`, `frobeniusPolyRat`	6
Theorems `bind₁_frobeniusPolyRat_wittPolynomial`, `bind₁_frobeniusPoly_wittPolynomial`, `coeff_frobenius`, `coeff_frobeniusFun`, `coeff_frobenius_charP`, `frobeniusEquiv_apply`, `frobeniusEquiv_symm_apply`, `frobeniusFun_isPoly`, `frobeniusPolyAux_eq`, `frobeniusPoly_zmod`, `frobenius_bijective`, `frobenius_eq_map_frobenius`, `frobenius_isPoly`, `frobenius_zmodp`, `ghostComponent_frobenius`, `ghostComponent_frobeniusFun`, `map_frobeniusPoly`, `key₁`, `key₂`	19
Total	25

WittVector

Definitions

Name	Category	Theorems
`frobenius` 📖	CompOp	17 math math: `iterate_verschiebung_mul`, `frobenius_isPoly`, `frobenius_bijective`, `frobenius_frobeniusRotation`, `frobenius_eq_map_frobenius`, `iterate_frobenius_coeff`, `iterate_verschiebung_iterate_frobenius`, `verschiebung_mul_frobenius`, `coeff_frobenius_charP`, `verschiebung_frobenius`, `ghostComponent_frobenius`, `verschiebung_frobenius_comm`, `iterate_verschiebung_mul_left`, `frobeniusEquiv_apply`, `coeff_frobenius`, `frobenius_verschiebung`, `frobenius_zmodp`
`frobeniusEquiv` 📖	CompOp	4 math math: `frobeniusEquiv_symm_apply`, `exists_frobenius_solution_fractionRing`, `exists_frobenius_solution_fractionRing_aux`, `frobeniusEquiv_apply`
`frobeniusFun` 📖	CompOp	3 math math: `ghostComponent_frobeniusFun`, `coeff_frobeniusFun`, `frobeniusFun_isPoly`
`frobeniusPoly` 📖	CompOp	5 math math: `bind₁_frobeniusPoly_wittPolynomial`, `frobeniusPoly_zmod`, `coeff_frobeniusFun`, `map_frobeniusPoly`, `coeff_frobenius`
`frobeniusPolyAux` 📖	CompOp	1 math math: `frobeniusPolyAux_eq`
`frobeniusPolyRat` 📖	CompOp	2 math math: `map_frobeniusPoly`, `bind₁_frobeniusPolyRat_wittPolynomial`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bind₁_frobeniusPolyRat_wittPolynomial` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPolynomial` `Rat.commSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id` `AlgHom.funLike` `MvPolynomial.bind₁` `frobeniusPolyRat` `wittPolynomial` `Rat.commRing`	—	`Rat.instCharZero` `MvPolynomial.bind₁_bind₁` `bind₁_xInTermsOfW_wittPolynomial` `MvPolynomial.bind₁_X_right`
`bind₁_frobeniusPoly_wittPolynomial` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `MvPolynomial` `Int.instCommSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id` `AlgHom.funLike` `MvPolynomial.bind₁` `frobeniusPoly` `wittPolynomial` `Int.instCommRing`	—	`MvPolynomial.map_injective` `Int.cast_injective` `Rat.instCharZero` `MvPolynomial.map_bind₁` `map_frobeniusPoly` `map_wittPolynomial` `bind₁_frobeniusPolyRat_wittPolynomial`
`coeff_frobenius` 📖	mathematical	—	`coeff` `DFunLike.coe` `RingHom` `WittVector` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `RingHom.instFunLike` `frobenius` `AlgHom` `MvPolynomial` `Int.instCommSemiring` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id` `Ring.toIntAlgebra` `CommRing.toRing` `AlgHom.funLike` `MvPolynomial.aeval` `frobeniusPoly`	—	`coeff_frobeniusFun`
`coeff_frobeniusFun` 📖	mathematical	—	`coeff` `frobeniusFun` `DFunLike.coe` `AlgHom` `MvPolynomial` `Int.instCommSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `CommRing.toCommSemiring` `MvPolynomial.algebra` `Algebra.id` `Ring.toIntAlgebra` `CommRing.toRing` `AlgHom.funLike` `MvPolynomial.aeval` `frobeniusPoly`	—	`frobeniusFun.eq_1`
`coeff_frobenius_charP` 📖	mathematical	—	`coeff` `DFunLike.coe` `RingHom` `WittVector` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `RingHom.instFunLike` `frobenius` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`coeff_frobenius` `MvPolynomial.aeval_eq_eval₂Hom` `MvPolynomial.eval₂Hom_map_hom` `MvPolynomial.eval₂Hom_congr` `RingHom.ext_int` `frobeniusPoly_zmod` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `MvPolynomial.aeval_X`
`frobeniusEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `WittVector` `instMul` `instAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `frobeniusEquiv` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `RingHom.instFunLike` `frobenius`	—	`expChar_prime`
`frobeniusEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `WittVector` `instMul` `instAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `frobeniusEquiv` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `RingHom.instFunLike` `map` `RingHomClass.toRingHom` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toAdd` `frobeniusEquiv`	—	`expChar_prime`
`frobeniusFun_isPoly` 📖	mathematical	—	`IsPoly` `frobeniusFun`	—	`coeff_frobeniusFun`
`frobeniusPolyAux_eq` 📖	mathematical	—	`frobeniusPolyAux` `MvPolynomial` `Int.instCommSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `MvPolynomial.instCommRingMvPolynomial` `Int.instCommRing` `MvPolynomial.X` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finset.range` `Monoid.toNatPow` `Nat.instMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `MvPolynomial.C` `Nat.choose` `multiplicity`	—	`frobeniusPolyAux.eq_1` `Fin.sum_univ_eq_sum_range`
`frobeniusPoly_zmod` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `Int.instCommSemiring` `ZMod` `Semifield.toCommSemiring` `Field.toSemifield` `ZMod.instField` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.map` `Int.castRingHom` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `ZMod.commRing` `frobeniusPoly` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MvPolynomial.X`	—	`frobeniusPoly.eq_1` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `MvPolynomial.map_X` `MvPolynomial.map_C` `eq_intCast` `Int.cast_natCast` `ZMod.natCast_self` `MvPolynomial.C_0` `MulZeroClass.zero_mul` `add_zero`
`frobenius_bijective` 📖	mathematical	—	`Function.Bijective` `WittVector` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `RingHom.instFunLike` `frobenius`	—	`expChar_prime` `RingEquiv.bijective`
`frobenius_eq_map_frobenius` 📖	mathematical	—	`frobenius` `map` `frobenius` `CommRing.toCommSemiring` `expChar_prime` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`RingHom.ext` `expChar_prime` `ext` `coeff_frobenius_charP`
`frobenius_isPoly` 📖	mathematical	—	`IsPoly` `DFunLike.coe` `RingHom` `WittVector` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `RingHom.instFunLike` `frobenius`	—	`frobeniusFun_isPoly`
`frobenius_zmodp` 📖	mathematical	—	`DFunLike.coe` `RingHom` `WittVector` `ZMod` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `ZMod.commRing` `RingHom.instFunLike` `frobenius`	—	`coeff_frobenius_charP` `ZMod.charP` `ZMod.pow_card`
`ghostComponent_frobenius` 📖	mathematical	—	`DFunLike.coe` `RingHom` `WittVector` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `RingHom.instFunLike` `ghostComponent` `frobenius`	—	`ghostComponent_frobeniusFun`
`ghostComponent_frobeniusFun` 📖	mathematical	—	`DFunLike.coe` `RingHom` `WittVector` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `RingHom.instFunLike` `ghostComponent` `frobeniusFun`	—	`MvPolynomial.aeval_bind₁`
`map_frobeniusPoly` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `Int.instCommSemiring` `Rat.commSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.map` `Int.castRingHom` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `Rat.commRing` `frobeniusPoly` `frobeniusPolyRat`	—	`frobeniusPoly.eq_1` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `MvPolynomial.map_C` `MvPolynomial.map_X` `eq_intCast` `Int.cast_natCast` `Rat.instCharZero` `frobeniusPolyRat.eq_1` `Nat.strong_induction_on` `xInTermsOfW_eq` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `map_sum` `Finset.sum_congr` `MvPolynomial.bind₁_C_right` `AlgHomClass.toRingHomClass` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `mul_pow` `mul_invOf_self` `one_pow` `MvPolynomial.bind₁_X_right` `wittPolynomial_eq_sum_C_mul_X_pow` `Finset.sum_range_succ` `tsub_self` `Nat.instOrderedSub` `add_tsub_cancel_left` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `pow_zero` `pow_one` `sub_mul` `add_mul` `Distrib.rightDistribClass` `mul_right_comm` `MvPolynomial.C_mul` `pow_succ'` `mul_assoc` `mul_one` `MvPolynomial.C_1` `one_mul` `add_comm` `add_assoc` `add_sub` `frobeniusPolyAux_eq` `mul_sub` `sub_eq_add_neg` `neg_eq_iff_eq_neg` `neg_sub` `Finset.sum_mul` `Finset.mul_sum` `Finset.mem_range` `add_pow` `Finset.sum_range_succ'` `tsub_zero` `Nat.choose_zero_right` `Nat.cast_one` `mul_add` `Distrib.leftDistribClass` `le_of_lt` `pow_mul` `add_sub_cancel_right` `mul_comm` `MvPolynomial.C_eq_coe_nat` `invOf_eq_inv` `inv_pow` `Nat.cast_mul` `Int.cast_mul` `Rat.natCast_div` `map_frobeniusPoly.key₁` `Nat.cast_pow` `Mathlib.Tactic.LinearCombination.eq_of_eq` `AddRightCancelSemigroup.toIsRightCancelAdd` `Mathlib.Tactic.LinearCombination.mul_const_eq` `map_frobeniusPoly.key₂` `LT.lt.le` `Mathlib.Tactic.LinearCombination.eq_rearrange` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `isReduced_of_noZeroDivisors` `IsStrictOrderedRing.noZeroDivisors` `Rat.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `Nat.Prime.ne_zero` `Fact.out` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `neg_div` `neg_mul` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `mul_neg` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.pow_one_cast` `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.zero_mul` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.cast_zero`

WittVector.map_frobeniusPoly

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`key₁` 📖	mathematical	`Monoid.toNatPow` `Nat.instMonoid`	`multiplicity` `Nat.choose`	—	`pow_dvd_of_le_emultiplicity` `Nat.Prime.emultiplicity_choose_prime_pow` `Fact.out` `le_refl`
`key₂` 📖	mathematical	`Monoid.toNatPow` `Nat.instMonoid`	`multiplicity`	—	`pow_multiplicity_dvd` `Nat.Prime.one_lt` `Fact.out` `LE.le.trans` `LT.lt.trans_le` `tsub_add_eq_add_tsub` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `add_comm` `add_tsub_assoc_of_le` `add_assoc` `tsub_right_comm` `tsub_add_cancel_of_le` `le_tsub_of_add_le_right` `le_tsub_iff_left`

---

← Back to Index