Theorems · Definition · number theory
Fermat42
ℤ → ℤ → ℤ → Prop
Shorthand for three non-zero integers a, b, and c satisfying a ^ 4 + b ^ 4 = c ^ 2.
We will show that no integers satisfy this equation. Clearly Fermat's Last theorem for n = 4
follows.
- Defined in
- Mathlib.NumberTheory.FLT.Four
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 35 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by10
Results whose statement or proof uses this declaration.
- Fermat42.Minimalproof · cited by 8
- Fermat42.coprime_of_minimalproof · cited by 2
- Fermat42.ne_zerostatement and proof · cited by 2
- Fermat42.commstatement · cited by 1
- Fermat42.exists_minimalstatement and proof · cited by 1
- Fermat42.exists_odd_minimalstatement and proof · cited by 1
- Fermat42.exists_pos_odd_minimalstatement and proof · cited by 1
- Fermat42.minimal_commproof · cited by 1
- Fermat42.mulstatement · cited by 1
- Fermat42.neg_of_minimalproof · cited by 1