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(linear_algebra/basic): some lemmas about span and restrict_scalars #10167

Closed
wants to merge 11 commits into from
Closed

[Merged by Bors] - feat(linear_algebra/basic): some lemmas about span and restrict_scalars #10167

wants to merge 11 commits into from

Commits on Nov 4, 2021

  1. feat(linear_algebra/basic): some lemmas about span and restrict_scalars

    @eric-wieser
    eric-wieser committed Nov 4, 2021
    Configuration menu
    Copy the full SHA
    1bbeaa9 View commit details
    Browse the repository at this point in the history

  2. Remove duplicate lemma

    @eric-wieser
    eric-wieser committed Nov 4, 2021
    Configuration menu
    Copy the full SHA
    55c1f4c View commit details
    Browse the repository at this point in the history

  3. Update src/linear_algebra/basic.lean

    @eric-wieser
    eric-wieser committed Nov 4, 2021
    Configuration menu
    Copy the full SHA
    6891a3e View commit details
    Browse the repository at this point in the history

  4. Update src/linear_algebra/basic.lean

    @eric-wieser
    eric-wieser committed Nov 4, 2021
    Configuration menu
    Copy the full SHA
    93b37e7 View commit details
    Browse the repository at this point in the history

Commits on Nov 5, 2021

  1. Update pi.lean

    @eric-wieser
    eric-wieser committed Nov 5, 2021
    Configuration menu
    Copy the full SHA
    0ecdcb4 View commit details
    Browse the repository at this point in the history

  2. explicit variables

    @eric-wieser
    eric-wieser committed Nov 5, 2021
    Configuration menu
    Copy the full SHA
    20a4181 View commit details
    Browse the repository at this point in the history

  3. Update basic.lean

    @eric-wieser
    eric-wieser committed Nov 5, 2021
    Configuration menu
    Copy the full SHA
    16d63af View commit details
    Browse the repository at this point in the history

  4. Update finsupp.lean

    @eric-wieser
    eric-wieser committed Nov 5, 2021
    Configuration menu
    Copy the full SHA
    e978d11 View commit details
    Browse the repository at this point in the history

  5. add restrict_scalars_self

    @eric-wieser
    eric-wieser committed Nov 5, 2021
    Configuration menu
    Copy the full SHA
    716748c View commit details
    Browse the repository at this point in the history

  6. Update src/linear_algebra/basic.lean

    @eric-wieser
    eric-wieser committed Nov 5, 2021
    Configuration menu
    Copy the full SHA
    452bc7c View commit details
    Browse the repository at this point in the history

Commits on Nov 7, 2021

  1. Merge remote-tracking branch 'origin/master' into eric-wieser/span-tower

    @eric-wieser
    eric-wieser committed Nov 7, 2021
    Configuration menu
    Copy the full SHA
    6dd3d65 View commit details
    Browse the repository at this point in the history