Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(linear_algebra): the direct sum of a submodule quotient is the quotient of the direct sum #17069

Closed
wants to merge 8 commits into from
Closed

[Merged by Bors] - feat(linear_algebra): the direct sum of a submodule quotient is the quotient of the direct sum #17069

wants to merge 8 commits into from

Commits on Oct 19, 2022

  1. feat(linear_algebra): the direct sum of a submodule quotient is the q… 

    …uotient of the direct sum

This defines the linear equivalence `submodule.quotient_pi` which allows us to interchange taking the direct sum and taking the quotient. This result is useful for defining the ideal norm.

Co-Authored-By: Alex J. Best <alex.j.best@gmail.com>
    @Vierkantor @alexjbest
    Vierkantor and alexjbest committed Oct 19, 2022
    Configuration menu
    Copy the full SHA
    6e10630 View commit details
    Browse the repository at this point in the history

Commits on Oct 20, 2022

  1. Π for data 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @Vierkantor @eric-wieser
    Vierkantor and eric-wieser committed Oct 20, 2022
    Configuration menu
    Copy the full SHA
    daece37 View commit details
    Browse the repository at this point in the history

  2. submodule.map is generic now

    @Vierkantor
    Vierkantor committed Oct 20, 2022
    Configuration menu
    Copy the full SHA
    d398222 View commit details
    Browse the repository at this point in the history

  3. refl lemma for submodule.quotient.equiv

    @Vierkantor
    Vierkantor committed Oct 20, 2022
    Configuration menu
    Copy the full SHA
    27f992d View commit details
    Browse the repository at this point in the history

  4. symm lemma for submodule.quotient.equiv

    @Vierkantor
    Vierkantor committed Oct 20, 2022
    Configuration menu
    Copy the full SHA
    a2efdd0 View commit details
    Browse the repository at this point in the history

  5. trans lemma for submodule.quotient.equiv

    @Vierkantor
    Vierkantor committed Oct 20, 2022
    Configuration menu
    Copy the full SHA
    cf8e7f9 View commit details
    Browse the repository at this point in the history

  6. Timeout fix: squeeze a simp

    @Vierkantor
    Vierkantor committed Oct 20, 2022
    Configuration menu
    Copy the full SHA
    f1b2a54 View commit details
    Browse the repository at this point in the history

  7. It seems linear_equiv.coe_trans can't be @[simp] yet, or we'll ge… 

    …t annoying timeouts due to the simp set not converging fast enough (?)
    @Vierkantor
    Vierkantor committed Oct 20, 2022
    Configuration menu
    Copy the full SHA
    a1b659b View commit details
    Browse the repository at this point in the history