Commit 2023-06-29 04:23 cac608bc

View on Github →

feat: port RingTheory.WittVector.FrobeniusFractionField (#5561)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/WittVector/FrobeniusFractionField.lean

added def WittVector.RecursionBase.solution

added theorem WittVector.RecursionBase.solution_nonzero

added theorem WittVector.RecursionBase.solution_pow

added theorem WittVector.RecursionBase.solution_spec'

added theorem WittVector.RecursionBase.solution_spec

added theorem WittVector.RecursionMain.root_exists

added def WittVector.RecursionMain.succNthDefiningPoly

added theorem WittVector.RecursionMain.succNthDefiningPoly_degree

added def WittVector.RecursionMain.succNthVal

added theorem WittVector.RecursionMain.succNthVal_spec'

added theorem WittVector.RecursionMain.succNthVal_spec

added theorem WittVector.exists_frobenius_solution_fractionRing

added theorem WittVector.exists_frobenius_solution_fractionRing_aux

added def WittVector.frobeniusRotation

added theorem WittVector.frobeniusRotation_nonzero

added theorem WittVector.frobenius_frobeniusRotation