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(LinearAlgebra): the Erdős-Kaplansky theorem #9159

Closed
wants to merge 20 commits into from
Closed

[Merged by Bors] - feat(LinearAlgebra): the Erdős-Kaplansky theorem #9159

wants to merge 20 commits into from

Commits on Dec 10, 2023

  1. refactor: Subfield of DivisionRing, not just Field

    @alreadydone
    alreadydone committed Dec 10, 2023
    Configuration menu
    Copy the full SHA
    7b18437 View commit details
    Browse the repository at this point in the history

  2. docstring + small eqLocus generalization

    @alreadydone
    alreadydone committed Dec 10, 2023
    Configuration menu
    Copy the full SHA
    5727181 View commit details
    Browse the repository at this point in the history

  3. feat: cardinality of Subfield.closure

    @alreadydone
    alreadydone committed Dec 10, 2023
    Configuration menu
    Copy the full SHA
    1b7e850 View commit details
    Browse the repository at this point in the history

  4. privatize

    @alreadydone
    alreadydone committed Dec 10, 2023
    Configuration menu
    Copy the full SHA
    3b260fe View commit details
    Browse the repository at this point in the history

  5. Mathlib.lean

    @alreadydone
    alreadydone committed Dec 10, 2023
    Configuration menu
    Copy the full SHA
    f2a3978 View commit details
    Browse the repository at this point in the history

  6. namespace Subfield & more private

    @alreadydone
    alreadydone committed Dec 10, 2023
    Configuration menu
    Copy the full SHA
    b499365 View commit details
    Browse the repository at this point in the history

Commits on Dec 17, 2023

  1. WIP

    @alreadydone
    alreadydone committed Dec 17, 2023
    Configuration menu
    Copy the full SHA
    1a241ab View commit details
    Browse the repository at this point in the history

Commits on Dec 20, 2023

  1. feat: Erdős-Kaplansky Theorem

    @alreadydone
    alreadydone committed Dec 20, 2023
    Configuration menu
    Copy the full SHA
    a475741 View commit details
    Browse the repository at this point in the history

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

    @alreadydone
    alreadydone committed Dec 20, 2023
    Configuration menu
    Copy the full SHA
    86c0da5 View commit details
    Browse the repository at this point in the history

  3. finish

    @alreadydone
    alreadydone committed Dec 20, 2023
    Configuration menu
    Copy the full SHA
    f1dd579 View commit details
    Browse the repository at this point in the history

Commits on Dec 21, 2023

  1. golf

    @alreadydone
    alreadydone committed Dec 21, 2023
    Configuration menu
    Copy the full SHA
    e1d3048 View commit details
    Browse the repository at this point in the history

Commits on Dec 27, 2023

  1. Merge branch 'master' into DimPiModule

    @alreadydone
    alreadydone committed Dec 27, 2023
    Configuration menu
    Copy the full SHA
    0b0a420 View commit details
    Browse the repository at this point in the history

  2. fix file name

    @alreadydone
    alreadydone committed Dec 27, 2023
    Configuration menu
    Copy the full SHA
    b5ef4dd View commit details
    Browse the repository at this point in the history

  3. change rank_pi_nat to max_aleph0_mk_le_rank_function_nat

    @alreadydone
    alreadydone committed Dec 27, 2023
    Configuration menu
    Copy the full SHA
    aec66cb View commit details
    Browse the repository at this point in the history

  4. Discard changes to Mathlib.lean

    @alreadydone
    alreadydone committed Dec 27, 2023
    Configuration menu
    Copy the full SHA
    8d7fa43 View commit details
    Browse the repository at this point in the history

  5. Discard changes to Mathlib/SetTheory/Cardinal/Algebraic.lean

    @alreadydone
    alreadydone committed Dec 27, 2023
    Configuration menu
    Copy the full SHA
    01767d9 View commit details
    Browse the repository at this point in the history

  6. change deprecated name

    @alreadydone
    alreadydone committed Dec 27, 2023
    Configuration menu
    Copy the full SHA
    1dc85c6 View commit details
    Browse the repository at this point in the history

  7. systematic rename: pi -> fun, mk -> card

    @alreadydone
    alreadydone committed Dec 27, 2023
    Configuration menu
    Copy the full SHA
    b2af569 View commit details
    Browse the repository at this point in the history

  8. fix

    @alreadydone
    alreadydone committed Dec 27, 2023
    Configuration menu
    Copy the full SHA
    647e529 View commit details
    Browse the repository at this point in the history

  9. add rank_lt_rank_dual(')

    @alreadydone
    alreadydone committed Dec 27, 2023
    Configuration menu
    Copy the full SHA
    f87fcb7 View commit details
    Browse the repository at this point in the history