YijunYuanHarderNarasimhan0.1.0

Formalization of Harder-Narasimhan theory
#math
Sort by
  1. Registry dependency.
    Found on Reservoir.

    mathlibv4.28.0

    The math library of Lean 4
  2. Registry dependency.
    Found on Reservoir.

    plausiblev4.28.0

  3. Registry dependency.
    Found on Reservoir.

    LeanSearchClientc5d5b8f

    Syntax for searching with natural language from Lean, using https://leansearch.net/ (may extend to other services)
  4. Registry dependency.
    Found on Reservoir.

    importGraphv4.28.0

    Tools to analyse and visualise the import structure of Lean packages and their files.
  5. Registry dependency.
    Found on Reservoir.

    proofwidgetsv0.0.87

    Helper toolkit for creating your own Lean 4 UserWidgets
  6. Registry dependency.
    Found on Reservoir.

    aesopv4.28.0

    White-box automation for Lean 4
  7. Registry dependency.
    Found on Reservoir.

    Qqv4.28.0

    Intuitive, type-safe expression quotations for Lean 4.
  8. Registry dependency.
    Found on Reservoir.

    batteriesv4.28.0

    The "batteries included" extended library for the Lean programming language and theorem prover