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(ring_theory/trace): Tr(x) is the sum of embeddings σ x into an algebraically closed field #8762

Closed
wants to merge 10 commits into from
Closed

[Merged by Bors] - feat(ring_theory/trace): Tr(x) is the sum of embeddings σ x into an algebraically closed field #8762

wants to merge 10 commits into from

Commits on Aug 24, 2021

  1. feat(field_theory/intermediate_field): generalize algebra instances 

    The `algebra` and `is_scalar_tower` instances for `intermediate_field` are (again) as general as those for `subalgebra`.
    @Vierkantor
    Vierkantor committed Aug 24, 2021
    Configuration menu
    Copy the full SHA
    41c42fe View commit details
    Browse the repository at this point in the history

  2. Lint fix

    @Vierkantor
    Vierkantor committed Aug 24, 2021
    Configuration menu
    Copy the full SHA
    232d8b9 View commit details
    Browse the repository at this point in the history

  3. Fix the timeout by making some unifications fail fast

    @Vierkantor
    Vierkantor committed Aug 24, 2021
    Configuration menu
    Copy the full SHA
    af3ffa7 View commit details
    Browse the repository at this point in the history

  4. Specialize intermediate_field.is_scalar_tower_mid 

    Use a specialized instance for the common case `is_scalar_tower K S L`, which
was the only instance in the old situation.
    @Vierkantor
    Vierkantor committed Aug 24, 2021
    Configuration menu
    Copy the full SHA
    fdad3dd View commit details
    Browse the repository at this point in the history

Commits on Aug 25, 2021

  1. chore(ring_theory/power_basis): @[simps] lift_equiv'

    @Vierkantor
    Vierkantor committed Aug 25, 2021
    Configuration menu
    Copy the full SHA
    a32df1c View commit details
    Browse the repository at this point in the history

  2. feat(field_theory): cardinality of alg_homs out of a finite separab… 

    …le extension
    @Vierkantor
    Vierkantor committed Aug 25, 2021
    Configuration menu
    Copy the full SHA
    f166b33 View commit details
    Browse the repository at this point in the history

  3. Golf/speedup

    @Vierkantor
    Vierkantor committed Aug 25, 2021
    Configuration menu
    Copy the full SHA
    2691f0b View commit details
    Browse the repository at this point in the history

  4. feat(ring_theory/trace): Tr(x) is the sum of embeddings σ x into an a… 

    …lgebraically closed field
    @Vierkantor
    Vierkantor committed Aug 25, 2021
    Configuration menu
    Copy the full SHA
    2fde8df View commit details
    Browse the repository at this point in the history

  5. More elegant proof 

    Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
    @Vierkantor @Ruben-VandeVelde
    Vierkantor and Ruben-VandeVelde committed Aug 25, 2021
    Configuration menu
    Copy the full SHA
    17ea68a View commit details
    Browse the repository at this point in the history

Commits on Aug 26, 2021

  1. Lint fix, by rearranging variables

    @Vierkantor
    Vierkantor committed Aug 26, 2021
    Configuration menu
    Copy the full SHA
    91372ec View commit details
    Browse the repository at this point in the history