English
There exists a descent framework that reduces FLT to a finite multiplicity analysis of λ in S'.c, with a base case forcing contradiction.
Русский
Существует нисходящая схема, сводящая ФFLT к конечной кратности λ в S'.c, приводящая к противоречию в базовом случае.
LaTeX
$$$\text{FLT}_{3\text{Gen}}(h)\Rightarrow \text{FLT}_3$$$
Lean4
/-- Pretty printer defined by `notation3` command. -/
@[local delab✝ app.IsUnit.unit]
public meta def _aux_Mathlib_NumberTheory_FLT_Three___delab_app__private_Mathlib_NumberTheory_FLT_Three_0_termη_1 :
Delab✝ :=
whenPPOption✝ getPPNotation✝ <|
whenNotPPOption✝ getPPExplicit✝ <|
withOverApp✝ 4
(getExpr✝ >>= fun e✝ =>
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `IsUnit.unit))
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `NumberField.RingOfIntegers))
(matchFVar✝ `K (matchExpr✝ isType'✝)))
pure✝))
pure✝)
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `IsPrimitiveRoot.toInteger))
(matchFVar✝ `K (matchExpr✝ isType'✝)))
pure✝)
(matchFVar✝ `ζ (matchFVar✝ `K (matchExpr✝ isType'✝))))
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `OfNat.ofNat))
(matchExpr✝ (Expr.isConstOf✝ · `Nat)))
(natLitMatcher✝ 3))
pure✝))
pure✝)
(matchFVar✝ `hζ
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `IsPrimitiveRoot))
(matchFVar✝ `K (matchExpr✝ isType'✝)))
pure✝)
(matchFVar✝ `ζ (matchFVar✝ `K (matchExpr✝ isType'✝))))
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `OfNat.ofNat))
(matchExpr✝ (Expr.isConstOf✝ · `Nat)))
(natLitMatcher✝ 3))
pure✝)))))
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `IsPrimitiveRoot.isUnit))
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `NumberField.RingOfIntegers))
(matchFVar✝ `K (matchExpr✝ isType'✝)))
pure✝))
pure✝)
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `OfNat.ofNat))
(matchExpr✝ (Expr.isConstOf✝ · `Nat)))
(natLitMatcher✝ 3))
pure✝))
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `IsPrimitiveRoot.toInteger))
(matchFVar✝ `K (matchExpr✝ isType'✝)))
pure✝)
(matchFVar✝ `ζ (matchFVar✝ `K (matchExpr✝ isType'✝))))
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `OfNat.ofNat))
(matchExpr✝ (Expr.isConstOf✝ · `Nat)))
(natLitMatcher✝ 3))
pure✝))
pure✝)
(matchFVar✝ `hζ
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `IsPrimitiveRoot))
(matchFVar✝ `K (matchExpr✝ isType'✝)))
pure✝)
(matchFVar✝ `ζ (matchFVar✝ `K (matchExpr✝ isType'✝))))
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `OfNat.ofNat))
(matchExpr✝ (Expr.isConstOf✝ · `Nat)))
(natLitMatcher✝ 3))
pure✝)))))
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `IsPrimitiveRoot.toInteger_isPrimitiveRoot))
(matchFVar✝ `K (matchExpr✝ isType'✝)))
pure✝)
(matchFVar✝ `ζ (matchFVar✝ `K (matchExpr✝ isType'✝))))
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `OfNat.ofNat))
(matchExpr✝ (Expr.isConstOf✝ · `Nat)))
(natLitMatcher✝ 3))
pure✝))
pure✝)
(matchFVar✝ `hζ
(matchApp✝
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `IsPrimitiveRoot))
(matchFVar✝ `K (matchExpr✝ isType'✝)))
pure✝)
(matchFVar✝ `ζ (matchFVar✝ `K (matchExpr✝ isType'✝))))
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `OfNat.ofNat))
(matchExpr✝ (Expr.isConstOf✝ · `Nat)))
(natLitMatcher✝ 3))
pure✝)))))
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `of_decide_eq_true))
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Ne)) (matchExpr✝ (Expr.isConstOf✝ · `Nat)))
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `OfNat.ofNat))
(matchExpr✝ (Expr.isConstOf✝ · `Nat)))
(natLitMatcher✝ 3))
pure✝))
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `OfNat.ofNat))
(matchExpr✝ (Expr.isConstOf✝ · `Nat)))
(natLitMatcher✝ 0))
pure✝)))
pure✝)
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `id))
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Eq)) (matchExpr✝ (Expr.isConstOf✝ · `Bool)))
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Decidable.decide))
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Ne))
(matchExpr✝ (Expr.isConstOf✝ · `Nat)))
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `OfNat.ofNat))
(matchExpr✝ (Expr.isConstOf✝ · `Nat)))
(natLitMatcher✝ 3))
pure✝))
(matchApp✝
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `OfNat.ofNat))
(matchExpr✝ (Expr.isConstOf✝ · `Nat)))
(natLitMatcher✝ 0))
pure✝)))
pure✝))
(matchExpr✝ (Expr.isConstOf✝ · `Bool.true))))
(matchApp✝
(matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Eq.refl)) (matchExpr✝ (Expr.isConstOf✝ · `Bool)))
(matchExpr✝ (Expr.isConstOf✝ · `Bool.true)))))) >=>
pure✝)
MatchState.empty✝ >>=
fun s✝ => withHeadRefIfTagAppFns✝ `(η))
