Documentation Verification Report

Four

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

Statistics

Metric	Count
Definitions `Fermat42`	1
Theorems `comm`, `coprime_of_minimal`, `exists_minimal`, `exists_odd_minimal`, `exists_pos_odd_minimal`, `minimal_comm`, `mul`, `ne_zero`, `neg_of_minimal`, `not_minimal`, `of_odd_primes`, `isCoprime_of_sq_sum`, `isCoprime_of_sq_sum'`, `fermatLastTheoremFour`, `not_fermat_42`	15
Total	16

Fermat42

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comm` 📖	mathematical	—	`Fermat42`	—	`add_comm`
`coprime_of_minimal` 📖	mathematical	`Minimal`	`IsCoprime` `Int.instCommSemiring`	—	`Int.isCoprime_iff_gcd_eq_one` `Nat.Prime.not_coprime_iff_dvd` `Int.natCast_dvd` `two_ne_zero` `Dvd.intro` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `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.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.mul_pf_right` `mul` `Nat.Prime.ne_zero` `lt_mul_iff_one_lt_left` `IsStrictOrderedRing.toMulPosStrictMono` `Nat.instIsStrictOrderedRing` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `ne_zero` `Nat.Prime.one_lt`
`exists_minimal` 📖	mathematical	`Fermat42`	`Minimal`	—	`Set.mem_setOf_eq` `Nat.find_spec` `Nat.find_min'`
`exists_odd_minimal` 📖	mathematical	`Fermat42`	`Minimal`	—	`exists_minimal` `Int.emod_two_eq_zero_or_one` `Int.isCoprime_iff_gcd_eq_one` `coprime_of_minimal` `minimal_comm`
`exists_pos_odd_minimal` 📖	mathematical	`Fermat42`	`Minimal`	—	`exists_odd_minimal` `lt_trichotomy` `ne_zero` `neg_of_minimal` `neg_pos` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Int.instAddLeftMono`
`minimal_comm` 📖	—	`Minimal`	—	—	`comm`
`mul` 📖	mathematical	—	`Fermat42` `Monoid.toNatPow` `Int.instMonoid`	—	`mul_ne_zero` `IsStrictOrderedRing.noZeroDivisors` `Int.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `Mathlib.Tactic.LinearCombination.eq_of_eq` `AddRightCancelSemigroup.toIsRightCancelAdd` `Mathlib.Tactic.LinearCombination.mul_const_eq` `Mathlib.Tactic.LinearCombination.eq_rearrange` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.pow_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.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Meta.NormNum.IsNat.of_raw` `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.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` `right_ne_zero_of_mul` `mul_right_inj'` `IsCancelMulZero.toIsLeftCancelMulZero` `Int.instIsCancelMulZero` `pow_ne_zero` `isReduced_of_noZeroDivisors`
`ne_zero` 📖	—	`Fermat42`	—	—	`ne_zero_pow` `two_ne_zero` `ne_of_gt` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `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.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Meta.NormNum.IsNat.of_raw` `add_pos` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Int.instAddLeftMono` `sq_pos_of_ne_zero` `Int.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `pow_ne_zero` `isReduced_of_noZeroDivisors` `IsStrictOrderedRing.noZeroDivisors`
`neg_of_minimal` 📖	—	`Minimal`	—	—	`neg_sq`
`not_minimal` 📖	—	`Minimal`	—	—	`Mathlib.Tactic.LinearCombination.eq_of_eq` `AddRightCancelSemigroup.toIsRightCancelAdd` `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.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `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.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.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.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` `Int.isCoprime_iff_gcd_eq_one` `IsCoprime.pow` `coprime_of_minimal` `sq` `PythagoreanTriple.coprime_classification'` `IsCoprime.of_mul_left_left` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.mul_one` `IsCoprime.add_mul_right_left` `IsCoprime.pow_left` `pow_ne_zero` `isReduced_of_noZeroDivisors` `IsStrictOrderedRing.noZeroDivisors` `Int.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `lt_of_le_of_ne` `Int.isCoprime_of_sq_sum'` `Int.Prime.dvd_pow'` `Nat.prime_two` `mul_assoc` `dvd_mul_right` `mul_right_inj'` `IsCancelMulZero.toIsLeftCancelMulZero` `Int.instIsCancelMulZero` `Int.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.LinearCombination.add_eq_eq` `Mathlib.Tactic.LinearCombination.mul_const_eq` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Meta.NormNum.isNat_mul` `Int.sq_of_gcd_eq_one` `neg_nonpos` `Int.instAddLeftMono` `sq_nonneg` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `not_lt` `mul_comm` `mul_nonneg_iff_of_pos_right` `IsStrictOrderedRing.toMulPosStrictMono` `le_of_lt` `lt_of_le_of_lt` `Int.natAbs_le_self_sq` `Int.le_self_sq` `lt_add_of_pos_right` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `sq_pos_of_ne_zero` `not_le_of_gt`

FermatLastTheorem

Theorems

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

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCoprime_of_sq_sum` 📖	mathematical	`IsCoprime` `instCommSemiring`	`Monoid.toNatPow` `instMonoid`	—	`sq` `IsCoprime.mul_add_left_left` `IsCoprime.mul_left`
`isCoprime_of_sq_sum'` 📖	mathematical	`IsCoprime` `instCommSemiring`	`Monoid.toNatPow` `instMonoid`	—	`IsCoprime.mul_right` `isCoprime_of_sq_sum` `isCoprime_comm` `add_comm`

(root)

Definitions

Name	Category	Theorems
`Fermat42` 📖	MathDef	2 math math: `Fermat42.comm`, `Fermat42.mul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fermatLastTheoremFour` 📖	mathematical	—	`FermatLastTheoremFor`	—	`fermatLastTheoremFor_iff_int` `not_fermat_42` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `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.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Meta.NormNum.IsNat.of_raw`
`not_fermat_42` 📖	—	—	—	—	`Fermat42.exists_pos_odd_minimal` `Fermat42.not_minimal`

---

← Back to Index