Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(RingTheory/Polynomial/HilbertPoly): the definition and key property of Polynomial.hilbertPoly p d for p : F[X] and d : ℕ, where F is a field. #19303

Closed
wants to merge 18 commits into from
Closed

[Merged by Bors] - feat(RingTheory/Polynomial/HilbertPoly): the definition and key property of Polynomial.hilbertPoly p d for p : F[X] and d : ℕ, where F is a field. #19303

wants to merge 18 commits into from

Commits on Nov 20, 2024

  1. defined hilbert polynomials

    @FMLJohn
    FMLJohn committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    a249cba View commit details
    Browse the repository at this point in the history

  2. removed unused imports

    @FMLJohn
    FMLJohn committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    6a38e38 View commit details
    Browse the repository at this point in the history

Commits on Nov 21, 2024

  1. lake exe shake --update

    @FMLJohn
    FMLJohn committed Nov 21, 2024
    Configuration menu
    Copy the full SHA
    950a378 View commit details
    Browse the repository at this point in the history

Commits on Nov 23, 2024

  1. omitted some variables

    @FMLJohn
    FMLJohn committed Nov 23, 2024
    Configuration menu
    Copy the full SHA
    5ad630a View commit details
    Browse the repository at this point in the history

Commits on Nov 26, 2024

  1. used ascPochhammer

    @FMLJohn
    FMLJohn committed Nov 26, 2024
    Configuration menu
    Copy the full SHA
    1890406 View commit details
    Browse the repository at this point in the history

  2. removed unused imports

    @FMLJohn
    FMLJohn committed Nov 26, 2024
    Configuration menu
    Copy the full SHA
    6e90216 View commit details
    Browse the repository at this point in the history

Commits on Nov 28, 2024

  1. generalised to arbitrary fields F with char(F) = 0

    @FMLJohn
    FMLJohn committed Nov 28, 2024
    Configuration menu
    Copy the full SHA
    bf4adde View commit details
    Browse the repository at this point in the history

Commits on Nov 30, 2024

  1. resolve conversations

    @FMLJohn
    FMLJohn committed Nov 30, 2024
    Configuration menu
    Copy the full SHA
    82615ab View commit details
    Browse the repository at this point in the history

  2. removed an unused import

    @FMLJohn
    FMLJohn committed Nov 30, 2024
    Configuration menu
    Copy the full SHA
    55826e8 View commit details
    Browse the repository at this point in the history

  3. added the namespace PowerSeries

    @FMLJohn
    FMLJohn committed Nov 30, 2024
    Configuration menu
    Copy the full SHA
    092e465 View commit details
    Browse the repository at this point in the history

  4. omitted a namespace

    @FMLJohn
    FMLJohn committed Nov 30, 2024
    Configuration menu
    Copy the full SHA
    af7f9b2 View commit details
    Browse the repository at this point in the history

  5. changed some explicitness

    @FMLJohn
    FMLJohn committed Nov 30, 2024
    Configuration menu
    Copy the full SHA
    564de1f View commit details
    Browse the repository at this point in the history

  6. added some lemmas

    @FMLJohn
    FMLJohn committed Nov 30, 2024
    Configuration menu
    Copy the full SHA
    f67f874 View commit details
    Browse the repository at this point in the history

Commits on Dec 1, 2024

  1. added hilbert_poly_succ

    @FMLJohn
    FMLJohn committed Dec 1, 2024
    Configuration menu
    Copy the full SHA
    cc71c8c View commit details
    Browse the repository at this point in the history

  2. moved Hilbert.lean

    @FMLJohn
    FMLJohn committed Dec 1, 2024
    Configuration menu
    Copy the full SHA
    4dbaf8a View commit details
    Browse the repository at this point in the history

  3. changed noshake

    @FMLJohn
    FMLJohn committed Dec 1, 2024
    Configuration menu
    Copy the full SHA
    585338c View commit details
    Browse the repository at this point in the history

Commits on Dec 2, 2024

  1. final changes

    @FMLJohn
    FMLJohn committed Dec 2, 2024
    Configuration menu
    Copy the full SHA
    1ee7ee6 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/master' into hilbert

    @FMLJohn
    FMLJohn committed Dec 2, 2024
    Configuration menu
    Copy the full SHA
    fe4cf0e View commit details
    Browse the repository at this point in the history