Documentation Verification Report

FrobeniusFractionField

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

Statistics

Metric	Count
Definitions `solution`, `succNthDefiningPoly`, `succNthVal`, `frobeniusRotation`, `frobeniusRotationCoeff`	5
Theorems `solution_nonzero`, `solution_pow`, `solution_spec`, `solution_spec'`, `root_exists`, `succNthDefiningPoly_degree`, `succNthVal_spec`, `succNthVal_spec'`, `exists_frobenius_solution_fractionRing`, `exists_frobenius_solution_fractionRing_aux`, `frobeniusRotation_nonzero`, `frobenius_frobeniusRotation`	12
Total	17

WittVector

Definitions

Name	Category	Theorems
`frobeniusRotation` 📖	CompOp	2 math math: `frobenius_frobeniusRotation`, `exists_frobenius_solution_fractionRing_aux`
`frobeniusRotationCoeff` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_frobenius_solution_fractionRing` 📖	mathematical	—	`FractionRing` `WittVector` `instCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `OreLocalization.instMul` `CommMonoid.toMonoid` `CommRing.toCommMonoid` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `OreLocalization.oreSetComm` `DFunLike.coe` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `OreLocalization.instCommRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `IsFractionRing.ringEquivOfRingEquiv` `OreLocalization.instAlgebra` `Algebra.id` `Localization.isLocalization` `frobeniusEquiv` `PerfectField.toPerfectRing` `IsAlgClosed.perfectField` `expChar_prime` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `OreLocalization.instDivisionRingNonZeroDivisors` `CommRing.toRing` `instNontrivial` `IsLocalRing.toNontrivial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Field.instIsLocalRing` `instNoZeroDivisorsOfCharP` `IsDomain.to_noZeroDivisors` `instIsDomain` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `OreLocalization.instRing`	—	`Localization.induction_on` `Localization.isLocalization` `PerfectField.toPerfectRing` `IsAlgClosed.perfectField` `expChar_prime` `instNontrivial` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `instNoZeroDivisorsOfCharP` `IsDomain.to_noZeroDivisors` `instIsDomain` `mem_nonZeroDivisors_iff_ne_zero` `IsDomain.toNontrivial` `instIsDomain` `FractionRing.mk_eq_div` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `zero_div` `exists_eq_pow_p_mul` `IsFractionRing.injective` `frobeniusRotation_nonzero` `exists_frobenius_solution_fractionRing_aux`
`exists_frobenius_solution_fractionRing_aux` 📖	mathematical	`WittVector` `Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors` `instMul` `hasNatPow` `instNatCast`	`Localization` `CommRing.toCommMonoid` `OreLocalization.instMul` `CommMonoid.toMonoid` `OreLocalization.oreSetComm` `DFunLike.coe` `RingEquiv` `FractionRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `OreLocalization.instCommRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `IsFractionRing.ringEquivOfRingEquiv` `OreLocalization.instAlgebra` `Algebra.id` `Localization.isLocalization` `frobeniusEquiv` `PerfectField.toPerfectRing` `IsAlgClosed.perfectField` `expChar_prime` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `RingHom` `OreLocalization.instSemiring` `RingHom.instFunLike` `algebraMap` `frobeniusRotation` `Monoid.toMulOneClass` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `OreLocalization.instDivisionRingNonZeroDivisors` `CommRing.toRing` `instNontrivial` `IsLocalRing.toNontrivial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Field.instIsLocalRing` `instNoZeroDivisorsOfCharP` `IsDomain.to_noZeroDivisors` `instIsDomain` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `OreLocalization.instRing`	—	`Mathlib.Tactic.LinearCombination.eq_of_eq` `AddRightCancelSemigroup.toIsRightCancelAdd` `frobenius_frobeniusRotation` `Mathlib.Tactic.LinearCombination.eq_rearrange` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.sub_pf` `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.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `zero_coeff` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `IsFractionRing.injective` `Localization.isLocalization` `PerfectField.toPerfectRing` `IsAlgClosed.perfectField` `expChar_prime` `instNontrivial` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `instNoZeroDivisorsOfCharP` `IsDomain.to_noZeroDivisors` `instIsDomain` `zpow_sub₀` `FractionRing.p_nonzero` `IsDomain.toNontrivial` `instIsDomain` `IsFractionRing.ringEquivOfRingEquiv_algebraMap` `FractionRing.mk_eq_div` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `map_natCast` `zpow_natCast` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `isReduced_of_noZeroDivisors` `Localization.instNoZeroDivisors` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial`
`frobeniusRotation_nonzero` 📖	—	—	—	—	`RecursionBase.solution_nonzero` `zero_coeff`
`frobenius_frobeniusRotation` 📖	mathematical	—	`WittVector` `instMul` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `RingHom.instFunLike` `frobenius` `frobeniusRotation`	—	`ext` `mul_coeff_zero` `coeff_frobenius_charP` `RecursionBase.solution_spec'` `nthRemainder_spec` `frobeniusRotationCoeff.eq_2` `RecursionMain.succNthVal_spec'` `TruncatedWittVector.ext` `coeff_truncateFun`

WittVector.RecursionBase

Definitions

Name	Category	Theorems
`solution` 📖	CompOp	2 math math: `solution_spec`, `solution_spec'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`solution_nonzero` 📖	—	—	—	—	`solution_spec` `div_eq_zero_iff` `zero_pow` `Nat.Prime.one_lt` `Fact.out`
`solution_pow` 📖	mathematical	—	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `WittVector.coeff`	—	`IsAlgClosed.exists_pow_nat_eq` `tsub_pos_of_lt` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `Nat.Prime.one_lt` `Fact.out`
`solution_spec` 📖	mathematical	—	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `solution` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `WittVector.coeff`	—	`solution_pow`
`solution_spec'` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `solution` `WittVector.coeff`	—	`solution_spec` `Nat.Prime.ne_zero` `Fact.out`

WittVector.RecursionMain

Definitions

Name	Category	Theorems
`succNthDefiningPoly` 📖	CompOp	3 math math: `succNthDefiningPoly_degree`, `succNthVal_spec`, `root_exists`
`succNthVal` 📖	CompOp	2 math math: `succNthVal_spec'`, `succNthVal_spec`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`root_exists` 📖	mathematical	—	`Polynomial.IsRoot` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `succNthDefiningPoly`	—	`IsAlgClosed.exists_root` `succNthDefiningPoly_degree` `instIsDomain` `WithBot.charZero` `Nat.instCharZero` `Nat.Prime.ne_zero` `Fact.out`
`succNthDefiningPoly_degree` 📖	mathematical	—	`Polynomial.degree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `succNthDefiningPoly` `WithBot` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne`	—	`Polynomial.degree_mul` `IsDomain.to_noZeroDivisors` `Polynomial.degree_C` `pow_ne_zero` `isReduced_of_noZeroDivisors` `Nat.instCanonicallyOrderedAdd` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instNontrivial` `Polynomial.degree_pow` `IsDomain.toNontrivial` `Polynomial.degree_X` `Nat.smul_one_eq_cast` `add_zero` `Polynomial.degree_sub_eq_left_of_degree_lt` `Nat.cast_one` `WithBot.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `WithBot.zeroLEOneClass` `Nat.instZeroLEOneClass` `WithBot.charZero` `Nat.instCharZero` `Nat.Prime.one_lt` `Fact.out` `succNthDefiningPoly.eq_1` `Polynomial.degree_add_eq_left_of_degree_lt` `lt_of_le_of_lt` `Polynomial.degree_C_le` `Nat.cast_zero` `Nat.Prime.pos`
`succNthVal_spec` 📖	mathematical	—	`Polynomial.IsRoot` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `succNthDefiningPoly` `succNthVal`	—	`root_exists`
`succNthVal_spec'` 📖	mathematical	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Distrib.toMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `succNthVal` `WittVector.coeff` `Nat.instMonoid` `WittVector.nthRemainder` `WittVector.truncateFun`	—	`sub_eq_zero` `succNthVal_spec` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `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.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.pow_one_cast` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.sub_pf` `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.Tactic.Ring.neg_zero` `Polynomial.eval_add` `Polynomial.eval_sub` `Polynomial.eval_mul` `Polynomial.eval_pow` `Polynomial.eval_X` `Polynomial.eval_C`

---

← Back to Index