Commit 2024-05-20 10:52 7bda946b

View on Github →

feat(NumberTheory.FLT.Three): basic properties of a solution to flt3 (#12977) We add Solution' and Solution, structures representing solutions to the generalized Fermat's equation FermatLastTheoremForThreeGen. The proof of flt3 will be a descent argument on a given Solution.

Estimated changes

Modified Mathlib/NumberTheory/FLT/Three.lean

added def FermatLastTheoremForThreeGen.Solution'.multiplicity

added theorem FermatLastTheoremForThreeGen.Solution'.multiplicity_lambda_c_finite

added structure FermatLastTheoremForThreeGen.Solution'

added theorem FermatLastTheoremForThreeGen.Solution.exists_minimal

added def FermatLastTheoremForThreeGen.Solution.isMinimal

added def FermatLastTheoremForThreeGen.Solution.multiplicity

added structure FermatLastTheoremForThreeGen.Solution