Theorems · Definition · number theory
Fermat42.Minimal
ℤ → ℤ → ℤ → Prop
We say a solution to a ^ 4 + b ^ 4 = c ^ 2 is minimal if there is no other solution with
a smaller c (in absolute value).
- Defined in
- Mathlib.NumberTheory.FLT.Four
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 36 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fermat42proof · cited by 9
Cited by8
Results whose statement or proof uses this declaration.
- Fermat42.coprime_of_minimalstatement and proof · cited by 2
- not_fermat_42proof · cited by 1
- Fermat42.exists_minimalstatement · cited by 1
- Fermat42.exists_odd_minimalstatement and proof · cited by 1
- Fermat42.exists_pos_odd_minimalstatement and proof · cited by 1
- Fermat42.minimal_commstatement and proof · cited by 1
- Fermat42.neg_of_minimalstatement and proof · cited by 1
- Fermat42.not_minimalstatement and proof · cited by 1