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: port FieldTheory.SplittingField.Construction #4891

Closed
wants to merge 22 commits into from
Closed

[Merged by Bors] - feat: port FieldTheory.SplittingField.Construction #4891

wants to merge 22 commits into from

Commits on Jun 9, 2023

  1. feat: port FieldTheory.SplittingField.Construction

    @ChrisHughes24
    ChrisHughes24 committed Jun 9, 2023
    Configuration menu
    Copy the full SHA
    8fca37c View commit details
    Browse the repository at this point in the history

  2. Initial file copy from mathport

    @ChrisHughes24
    ChrisHughes24 committed Jun 9, 2023
    Configuration menu
    Copy the full SHA
    2388ba3 View commit details
    Browse the repository at this point in the history

  3. automated fixes 

    Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
    @ChrisHughes24
    ChrisHughes24 committed Jun 9, 2023
    Configuration menu
    Copy the full SHA
    a0d78ca View commit details
    Browse the repository at this point in the history

  4. Prove existence of SplittingField

    @ChrisHughes24
    ChrisHughes24 committed Jun 9, 2023
    Configuration menu
    Copy the full SHA
    975919e View commit details
    Browse the repository at this point in the history

  5. define SplittingField

    @ChrisHughes24
    ChrisHughes24 committed Jun 9, 2023
    Configuration menu
    Copy the full SHA
    45c686e View commit details
    Browse the repository at this point in the history

  6. Prove IsScalarTower

    @ChrisHughes24
    ChrisHughes24 committed Jun 9, 2023
    Configuration menu
    Copy the full SHA
    6a117ea View commit details
    Browse the repository at this point in the history

Commits on Jun 10, 2023

  1. use rootSet

    @ChrisHughes24
    ChrisHughes24 committed Jun 10, 2023
    Configuration menu
    Copy the full SHA
    610c773 View commit details
    Browse the repository at this point in the history

  2. fix build

    @ChrisHughes24
    ChrisHughes24 committed Jun 10, 2023
    Configuration menu
    Copy the full SHA
    9d9d027 View commit details
    Browse the repository at this point in the history

  3. small progress

    @ChrisHughes24
    ChrisHughes24 committed Jun 10, 2023
    Configuration menu
    Copy the full SHA
    27583d1 View commit details
    Browse the repository at this point in the history

  4. add scalar tower instance in MvPolynomial

    @ChrisHughes24
    ChrisHughes24 committed Jun 10, 2023
    Configuration menu
    Copy the full SHA
    7737b38 View commit details
    Browse the repository at this point in the history

  5. finish modulo a few sorries

    @ChrisHughes24
    ChrisHughes24 committed Jun 10, 2023
    Configuration menu
    Copy the full SHA
    5458307 View commit details
    Browse the repository at this point in the history

  6. fix some yellow

    @ChrisHughes24
    ChrisHughes24 committed Jun 10, 2023
    Configuration menu
    Copy the full SHA
    3e78d8e View commit details
    Browse the repository at this point in the history

  7. delete duplicate instance

    @ChrisHughes24
    ChrisHughes24 committed Jun 10, 2023
    Configuration menu
    Copy the full SHA
    c3dd6ee View commit details
    Browse the repository at this point in the history

Commits on Jun 12, 2023

  1. minor cleanup

    Scott Morrison committed Jun 12, 2023
    Configuration menu
    Copy the full SHA
    d030bd0 View commit details
    Browse the repository at this point in the history

  2. most of the field instance

    Scott Morrison committed Jun 12, 2023
    Configuration menu
    Copy the full SHA
    084dda3 View commit details
    Browse the repository at this point in the history

  3. Prove qsmul_eq_mul'

    @ChrisHughes24
    ChrisHughes24 committed Jun 12, 2023
    Configuration menu
    Copy the full SHA
    c5d672e View commit details
    Browse the repository at this point in the history

Commits on Jun 13, 2023

  1. Update Mathlib/FieldTheory/SplittingField/IsSplittingField.lean 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @jcommelin @eric-wieser
    jcommelin and eric-wieser committed Jun 13, 2023
    Configuration menu
    Copy the full SHA
    c4a55f5 View commit details
    Browse the repository at this point in the history

  2. adjoin_rootSet everywhere

    @jcommelin
    jcommelin committed Jun 13, 2023
    Configuration menu
    Copy the full SHA
    ae712c9 View commit details
    Browse the repository at this point in the history

  3. and a bit more adjoin_rootSet

    @jcommelin
    jcommelin committed Jun 13, 2023
    Configuration menu
    Copy the full SHA
    828cd04 View commit details
    Browse the repository at this point in the history

  4. minitweak

    @jcommelin
    jcommelin committed Jun 13, 2023
    Configuration menu
    Copy the full SHA
    0505a4d View commit details
    Browse the repository at this point in the history

  5. fix final sorry

    @jcommelin
    jcommelin committed Jun 13, 2023
    Configuration menu
    Copy the full SHA
    022d6a6 View commit details
    Browse the repository at this point in the history

Commits on Jun 14, 2023

  1. Merge branch 'master' into port/FieldTheory.SplittingField.Construction

    @eric-wieser
    eric-wieser committed Jun 14, 2023
    Configuration menu
    Copy the full SHA
    90124bb View commit details
    Browse the repository at this point in the history