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] - golf(data/polynomial): factorization into linear factors when #roots=degree #14862

Closed
wants to merge 9 commits into from
Closed

[Merged by Bors] - golf(data/polynomial): factorization into linear factors when #roots=degree #14862

wants to merge 9 commits into from

Commits on Jun 20, 2022

  1. generalize

    @alreadydone
    alreadydone committed Jun 20, 2022
    Configuration menu
    Copy the full SHA
    3754147 View commit details
    Browse the repository at this point in the history

  2. eq_leading_coeff_mul_of_monic_of_dvd_of_degree_le

    @alreadydone
    alreadydone committed Jun 20, 2022
    Configuration menu
    Copy the full SHA
    9043331 View commit details
    Browse the repository at this point in the history

  3. remove is_domain

    @alreadydone
    alreadydone committed Jun 20, 2022
    Configuration menu
    Copy the full SHA
    99f17d8 View commit details
    Browse the repository at this point in the history

  4. slight golf

    @alreadydone
    alreadydone committed Jun 20, 2022
    Configuration menu
    Copy the full SHA
    1064baf View commit details
    Browse the repository at this point in the history

  5. K,L to A,B

    @alreadydone
    alreadydone committed Jun 20, 2022
    Configuration menu
    Copy the full SHA
    23d673a View commit details
    Browse the repository at this point in the history

Commits on Jun 21, 2022

  1. golf prod_multiset_X_sub_C_of_monic+roots_card_eq

    @alreadydone
    alreadydone committed Jun 21, 2022
    Configuration menu
    Copy the full SHA
    25494ad View commit details
    Browse the repository at this point in the history

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

    @alreadydone
    alreadydone committed Jun 21, 2022
    Configuration menu
    Copy the full SHA
    268dea3 View commit details
    Browse the repository at this point in the history

  3. separable.lean: X_sub -> X_sub_C

    @alreadydone
    alreadydone committed Jun 21, 2022
    Configuration menu
    Copy the full SHA
    fb11454 View commit details
    Browse the repository at this point in the history

  4. fixed.lean: X_sub -> X_sub_C

    @alreadydone
    alreadydone committed Jun 21, 2022
    Configuration menu
    Copy the full SHA
    ddccd00 View commit details
    Browse the repository at this point in the history