_aux_Mathlib_NumberTheory_FLT_Three___delab_app__private_Mathlib_NumberTheory_FLT_Three_0_termλ_1

English
In the three-gen framework, the multiplicity of λ in S'.c is at least 2.
Русский
В трёхгенераторной схеме кратность λ в S'.c не меньше 2.
LaTeX
$$$2 \le S'.multiplicity$$$
Lean4
/-- Pretty printer defined by `notation3` command. -/
@[local delab✝ app.HSub.hSub]
public meta def «_aux_Mathlib_NumberTheory_FLT_Three___delab_app__private_Mathlib_NumberTheory_FLT_Three_0_termλ_1» :
    Delab✝ :=
  whenPPOption✝ getPPNotation✝ <|
    whenNotPPOption✝ getPPExplicit✝ <|
      withOverApp✝ 6
        (getExpr✝ >>= fun e✝ =>
          (matchApp✝
                  (matchApp✝
                    (matchApp✝
                      (matchApp✝
                        (matchApp✝
                          (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `HSub.hSub))
                            (matchApp✝
                              (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `NumberField.RingOfIntegers))
                                (matchFVar✝ `K (matchExpr✝ isType'✝)))
                              pure✝))
                          (matchApp✝
                            (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `NumberField.RingOfIntegers))
                              (matchFVar✝ `K (matchExpr✝ isType'✝)))
                            pure✝))
                        (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✝ (matchExpr✝ (Expr.isConstOf✝ · `OfNat.ofNat))
                        (matchApp✝
                          (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `NumberField.RingOfIntegers))
                            (matchFVar✝ `K (matchExpr✝ isType'✝)))
                          pure✝))
                      (natLitMatcher✝ 1))
                    pure✝) >=>
                pure✝)
              MatchState.empty✝ >>=
            fun s✝ => withHeadRefIfTagAppFns✝ `(λ))
Похожие утверждения