Commit 2026-03-23 07:23 1727ba1c

View on Github →

chore(FLT/Three): remove backward.privateInPublic (#36982) This file exists solely to prove fermatLastTheoremThree, so all other declarations should not be public or exposed.

Estimated changes

Modified Mathlib/NumberTheory/FLT/Three.lean

added theorem FermatLastTheoremForThreeGen.Solution.X_ne_zero

added theorem FermatLastTheoremForThreeGen.Solution.X_u₁_spec

added theorem FermatLastTheoremForThreeGen.Solution.Y_u₂_spec

added theorem FermatLastTheoremForThreeGen.Solution.Z_u₃_spec

added theorem FermatLastTheoremForThreeGen.Solution.exists_cube_associated

added theorem FermatLastTheoremForThreeGen.Solution.formula1

added theorem FermatLastTheoremForThreeGen.Solution.formula2

added theorem FermatLastTheoremForThreeGen.Solution.formula3

added theorem FermatLastTheoremForThreeGen.Solution.isCoprime_Y_Z

added theorem FermatLastTheoremForThreeGen.Solution.isCoprime_helper

added theorem FermatLastTheoremForThreeGen.Solution.isCoprime_x_y

added theorem FermatLastTheoremForThreeGen.Solution.isCoprime_x_z

added theorem FermatLastTheoremForThreeGen.Solution.isCoprime_y_z

added theorem FermatLastTheoremForThreeGen.Solution.lambda_not_dvd_X

added theorem FermatLastTheoremForThreeGen.Solution.lambda_not_dvd_Y

added theorem FermatLastTheoremForThreeGen.Solution.lambda_not_dvd_Z

added theorem FermatLastTheoremForThreeGen.Solution.lambda_not_dvd_w

added theorem FermatLastTheoremForThreeGen.Solution.lambda_not_dvd_x

added theorem FermatLastTheoremForThreeGen.Solution.lambda_not_dvd_y

added theorem FermatLastTheoremForThreeGen.Solution.lambda_not_dvd_z

added theorem FermatLastTheoremForThreeGen.Solution.lambda_pow_dvd_a_add_b

added theorem FermatLastTheoremForThreeGen.Solution.lambda_sq_div_u₅_mul

added theorem FermatLastTheoremForThreeGen.Solution.u₄_def

added theorem FermatLastTheoremForThreeGen.Solution.u₄_eq_one_or_neg_one

added theorem FermatLastTheoremForThreeGen.Solution.u₄_sq

added theorem FermatLastTheoremForThreeGen.Solution.u₅_def

added theorem FermatLastTheoremForThreeGen.Solution.w_spec

added theorem FermatLastTheoremForThreeGen.Solution.x_mul_y_mul_z_eq_u_mul_w_cube

added theorem FermatLastTheoremForThreeGen.Solution.x_spec

added theorem FermatLastTheoremForThreeGen.Solution.y_spec

added theorem FermatLastTheoremForThreeGen.Solution.z_spec

added theorem cube_of_castHom_ne_zero

added theorem cube_of_not_dvd

deleted theorem fermatLastTheoremThree

added theorem fermatLastTheoremThree_of_dvd_a_of_gcd_eq_one_of_case2

added theorem three_dvd_b_of_dvd_a_of_gcd_eq_one_of_case2