∫ Утверждение Mathlib

_aux_Mathlib_RingTheory_Spectrum_Prime_ChevalleyComplexity___delab_app__private_Mathlib_RingTheory_Spectrum_Prime_ChevalleyComplexity_0_ChevalleyThm_PolynomialC_termCoeff(_)_1

Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

URI: https://scilib.ai/kg/mathlib#ChevalleyThm.PolynomialC._aux_Mathlib_RingTheory_Spectrum_Prime_ChevalleyComplexity___delab_app__private_Mathlib_RingTheory_Spectrum_Prime_ChevalleyComplexity_0_ChevalleyThm_PolynomialC_termCoeff(_)_1

← MathLib Explorer

Lean4

/-- Pretty printer defined by `notation3` command. -/
@[local delab✝ app.Set.range]
public meta def
  «_aux_Mathlib_RingTheory_Spectrum_Prime_ChevalleyComplexity___delab_app__private_Mathlib_RingTheory_Spectrum_Prime_ChevalleyComplexity_0_ChevalleyThm_PolynomialC_termCoeff(_)_1» :
    Delab✝ :=
  whenPPOption✝ getPPNotation✝ <|
    whenNotPPOption✝ getPPExplicit✝ <|
      withOverApp✝ 3
        (getExpr✝ >>= fun e✝ =>
          (matchApp✝
                  (matchApp✝ (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Set.range)) pure✝)
                    (matchExpr✝ (Expr.isConstOf✝ · `Nat)))
                  (matchApp✝ (matchApp✝ (matchApp✝ (matchExpr✝ (Expr.isConstOf✝ · `Polynomial.coeff)) pure✝) pure✝)
                    (matchVar✝ `p)) >=>
                pure✝)
              MatchState.empty✝ >>=
            fun s✝ => MatchState.delabVar✝ s✝ `p (some✝ e✝) >>= fun p => withHeadRefIfTagAppFns✝ `(coeff($p)))

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