_aux_Mathlib_FieldTheory_KummerExtension___delab_app_KummerExtension_termK[_√_]_1

English

In a suitable extension, X^n − C a splits into linear factors corresponding to the n-th roots of a multiplied by a fixed α with α^n = a.

Русский

В подходящем расширении X^n − C a раскладывается на линейные множители, соответствующие корням n-й степени a, умноженным на фиксированное α с α^n = a.

LaTeX

$$$X^n - C a = \\prod_{i=0}^{n-1} (X - C(ζ^i α))$ in an appropriate extension.$$

Lean4

/-- Pretty printer defined by `notation3` command. -/
@[scoped delab✝ app.AdjoinRoot]
public meta def «_aux_Mathlib_FieldTheory_KummerExtension___delab_app_KummerExtension_termK[_√_]_1» : Delab✝ :=
  whenPPOption✝ getPPNotation✝ <|
    whenNotPPOption✝ getPPExplicit✝ <|
      withOverApp✝ 3
        (getExpr✝ >>= fun e✝ =>
          (matchApp✝ (matchApp✝ (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `AdjoinRoot)) pure✝) pure✝)
                  (matchApp✝
                    (matchApp✝
                      (matchApp✝
                        (matchApp✝
                          (matchApp✝
                            (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `HSub.hSub))
                              (matchApp✝ (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Polynomial)) pure✝) pure✝))
                            (matchApp✝ (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Polynomial)) pure✝) pure✝))
                          (matchApp✝ (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Polynomial)) pure✝) pure✝))
                        pure✝)
                      (matchApp✝
                        (matchApp✝
                          (matchApp✝
                            (matchApp✝
                              (matchApp✝
                                (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `HPow.hPow))
                                  (matchApp✝ (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Polynomial)) pure✝) pure✝))
                                (matchExpr✝ (Expr.isConstOf✝ · `Nat)))
                              (matchApp✝ (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Polynomial)) pure✝) pure✝))
                            pure✝)
                          (matchApp✝ (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Polynomial.X)) pure✝) pure✝))
                        (matchVar✝ `n)))
                    (matchApp✝
                      (matchApp✝
                        (matchApp✝
                          (matchApp✝
                            (matchApp✝
                              (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `DFunLike.coe))
                                (matchApp✝
                                  (matchApp✝
                                    (matchApp✝ (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `RingHom)) pure✝)
                                      (matchApp✝ (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Polynomial)) pure✝) pure✝))
                                    pure✝)
                                  pure✝))
                              pure✝)
                            (matchLambda✝ pure✝
                              (fun n✝ =>
                                matchApp✝¹ (matchApp✝¹ (matchExpr✝¹ (Expr.isConstOf✝¹ · `Polynomial)) pure✝¹) pure✝¹)))
                          pure✝)
                        (matchApp✝ (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Polynomial.C)) pure✝) pure✝))
                      (matchVar✝ `a))) >=>
                pure✝)
              MatchState.empty✝ >>=
            fun s✝ =>
            MatchState.delabVar✝ s✝ `n (some✝ e✝) >>= fun n =>
              MatchState.delabVar✝ s✝ `a (some✝ e✝) >>= fun a => withHeadRefIfTagAppFns✝ `(K[$n√$a]))

Похожие утверждения