Documentation Verification Report

Basic

📁 Source: Mathlib/NumberTheory/FLT/Basic.lean

Statistics

Metric	Count
Definitions `FermatLastTheorem`, `FermatLastTheoremFor`, `FermatLastTheoremWith`, `FermatLastTheoremWith'`	4
Theorems `mono`, `fermatLastTheoremWith`, `fermatLastTheoremWith'`, `mono`, `dvd_c_of_prime_of_dvd_a_of_dvd_b_of_FLT`, `fermatLastTheoremFor_iff_int`, `fermatLastTheoremFor_iff_nat`, `fermatLastTheoremFor_iff_rat`, `fermatLastTheoremFor_zero`, `fermatLastTheoremWith'_iff_fermatLastTheoremWith`, `fermatLastTheoremWith'_nat_int_tfae`, `fermatLastTheoremWith'_of_semifield`, `fermatLastTheoremWith_nat_int_rat_tfae`, `fermatLastTheoremWith_of_fermatLastTheoremWith_coprime`, `isCoprime_of_gcd_eq_one_of_FLT`, `not_fermatLastTheoremFor_one`, `not_fermatLastTheoremFor_two`	17
Total	21

FermatLastTheoremFor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mono` 📖	—	`FermatLastTheoremFor`	—	—	`FermatLastTheoremWith.mono` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd`

FermatLastTheoremWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fermatLastTheoremWith'` 📖	mathematical	`FermatLastTheoremWith` `CommSemiring.toSemiring`	`FermatLastTheoremWith'`	—	—
`mono` 📖	—	`FermatLastTheoremWith`	—	—	`pow_mul'` `pow_ne_zero` `isReduced_of_noZeroDivisors`

FermatLastTheoremWith'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fermatLastTheoremWith` 📖	mathematical	`FermatLastTheoremWith'`	`FermatLastTheoremWith` `CommSemiring.toSemiring`	—	`mul_right_cancel₀` `IsCancelMulZero.toIsRightCancelMulZero` `IsDomain.toIsCancelMulZero` `pow_ne_zero` `isReduced_of_noZeroDivisors` `IsDomain.to_noZeroDivisors` `right_ne_zero_of_mul` `add_mul` `Distrib.rightDistribClass` `mul_pow`

(root)

Definitions

Name	Category	Theorems
`FermatLastTheorem` 📖	MathDef	1 math math: `FermatLastTheorem.of_odd_primes`
`FermatLastTheoremFor` 📖	MathDef	11 math math: `not_fermatLastTheoremFor_one`, `fermatLastTheoremFor_iff_rat`, `fermatLastTheoremFor_zero`, `fermatLastTheoremThree`, `FermatLastTheoremForThree_of_FermatLastTheoremThreeGen`, `not_fermatLastTheoremFor_two`, `fermatLastTheoremFor_iff_int`, `fermatLastTheoremFour`, `fermatLastTheoremFor_iff_nat`, `fermatLastTheoremThree_of_three_dvd_only_c`, `fermatLastTheoremWith'_nat_int_tfae`
`FermatLastTheoremWith` 📖	MathDef	7 math math: `fermatLastTheoremFor_iff_rat`, `fermatLastTheoremWith'_iff_fermatLastTheoremWith`, `fermatLastTheoremFor_iff_int`, `fermatLastTheoremWith_nat_int_rat_tfae`, `fermatLastTheoremFor_iff_nat`, `fermatLastTheoremWith_of_fermatLastTheoremWith_coprime`, `FermatLastTheoremWith'.fermatLastTheoremWith`
`FermatLastTheoremWith'` 📖	MathDef	5 math math: `FermatLastTheoremWith.fermatLastTheoremWith'`, `fermatLastTheoremWith'_iff_fermatLastTheoremWith`, `fermatLastTheoremWith'_polynomial`, `fermatLastTheoremWith'_of_semifield`, `fermatLastTheoremWith'_nat_int_tfae`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dvd_c_of_prime_of_dvd_a_of_dvd_b_of_FLT` 📖	—	`Prime` `CommSemiring.toCommMonoidWithZero` `Int.instCommSemiring` `Monoid.toNatPow` `Int.instMonoid`	—	—	`eq_or_ne` `pow_zero` `Int.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `Prime.dvd_of_dvd_pow` `dvd_neg` `dvd_add` `Distrib.leftDistribClass` `dvd_pow` `add_eq_zero_iff_eq_neg`
`fermatLastTheoremFor_iff_int` 📖	mathematical	—	`FermatLastTheoremFor` `FermatLastTheoremWith` `Int.instSemiring`	—	`List.TFAE.out` `fermatLastTheoremWith_nat_int_rat_tfae`
`fermatLastTheoremFor_iff_nat` 📖	mathematical	—	`FermatLastTheoremFor` `FermatLastTheoremWith` `Nat.instSemiring`	—	—
`fermatLastTheoremFor_iff_rat` 📖	mathematical	—	`FermatLastTheoremFor` `FermatLastTheoremWith` `Rat.semiring`	—	`List.TFAE.out` `fermatLastTheoremWith_nat_int_rat_tfae`
`fermatLastTheoremFor_zero` 📖	mathematical	—	`FermatLastTheoremFor`	—	`pow_zero` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat`
`fermatLastTheoremWith'_iff_fermatLastTheoremWith` 📖	mathematical	—	`FermatLastTheoremWith'` `FermatLastTheoremWith` `CommSemiring.toSemiring`	—	`FermatLastTheoremWith'.fermatLastTheoremWith` `FermatLastTheoremWith.fermatLastTheoremWith'`
`fermatLastTheoremWith'_nat_int_tfae` 📖	mathematical	—	`List.TFAE` `FermatLastTheoremFor` `FermatLastTheoremWith'` `Nat.instCommSemiring` `Int.instCommSemiring`	—	`fermatLastTheoremWith'_iff_fermatLastTheoremWith` `Nat.instIsDomain` `one_pow` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `fermatLastTheoremFor_iff_int` `Int.instIsDomain` `pow_zero` `Int.instCharZero` `Int.isUnit_iff` `isUnit_pow_iff` `List.tfae_of_cycle`
`fermatLastTheoremWith'_of_semifield` 📖	mathematical	—	`FermatLastTheoremWith'` `Semifield.toCommSemiring`	—	`mul_one` `Ne.isUnit`
`fermatLastTheoremWith_nat_int_rat_tfae` 📖	mathematical	—	`List.TFAE` `FermatLastTheoremWith` `Nat.instSemiring` `Int.instSemiring` `Rat.semiring`	—	`Nat.even_or_odd` `ne_of_gt` `Nat.cast_add` `Nat.cast_pow` `Int.natCast_natAbs` `Even.pow_abs` `IsStrictOrderedRing.toIsOrderedRing` `Int.instIsStrictOrderedRing` `Ne.lt_or_gt` `abs_of_neg` `Int.instAddLeftMono` `neg_pow` `Distrib.leftDistribClass` `LT.lt.not_gt` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `IsStrictOrderedRing.toZeroLEOneClass` `Eq.trans_lt` `add_neg` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Odd.pow_neg` `AddGroup.existsAddOfLE` `Mathlib.Meta.Positivity.int_natAbs_pos` `abs_of_pos` `Odd.neg_pow` `add_pos'` `mul_ne_zero` `IsStrictOrderedRing.noZeroDivisors` `Rat.num_ne_zero` `Nat.cast_pos'` `Int.instZeroLEOneClass` `mul_pos` `Rat.instIsStrictOrderedRing` `Rat.instAddLeftMono` `Rat.instZeroLEOneClass` `NeZero.one` `Rat.nontrivial` `Int.cast_injective` `Rat.instCharZero` `div_left_inj'` `Int.cast_add` `Int.cast_pow` `Int.cast_mul` `Int.cast_natCast` `add_div` `mul_div_mul_comm` `Rat.num_div_den` `div_self` `mul_one` `one_mul` `Nat.cast_zero` `List.tfae_of_cycle`
`fermatLastTheoremWith_of_fermatLastTheoremWith_coprime` 📖	mathematical	—	`FermatLastTheoremWith` `CommSemiring.toSemiring`	—	`Finset.gcd_dvd` `IsDomain.to_noZeroDivisors` `Finset.normalize_gcd` `normalize_eq_one` `normalize_associated` `mul_left_cancel₀` `IsCancelMulZero.toIsLeftCancelMulZero` `IsDomain.toIsCancelMulZero` `normalize_eq_zero` `Finset.gcd_mul_left` `Finset.gcd_eq_gcd_image` `Finset.image_insert` `Finset.image_singleton` `mul_right_inj'` `pow_ne_zero` `isReduced_of_noZeroDivisors` `mul_add` `Distrib.leftDistribClass` `mul_pow`
`isCoprime_of_gcd_eq_one_of_FLT` 📖	mathematical	`Finset.gcd` `CommSemiring.toCommMonoidWithZero` `Int.instCommSemiring` `Int.instNormalizedGCDMonoid` `Finset` `Finset.instInsert` `Finset.instSingleton` `Monoid.toNatPow` `Int.instMonoid`	`IsCoprime`	—	`eq_or_ne` `pow_zero` `Int.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `isCoprime_of_prime_dvd` `Int.instIsDomain` `EuclideanDomain.to_principal_ideal_domain` `zero_pow` `add_zero` `zero_add` `isReduced_of_noZeroDivisors` `IsStrictOrderedRing.noZeroDivisors` `Int.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `Finset.insert_eq_of_mem` `Finset.gcd_singleton` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `Prime.not_dvd_one` `Finset.dvd_gcd_iff` `dvd_c_of_prime_of_dvd_a_of_dvd_b_of_FLT`
`not_fermatLastTheoremFor_one` 📖	mathematical	—	`FermatLastTheoremFor`	—	`Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `one_pow` `pow_one`
`not_fermatLastTheoremFor_two` 📖	mathematical	—	`FermatLastTheoremFor`	—	`Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat`

---

← Back to Index