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/*): add lemma linear_independent.finite_of_is_noetherian #14714

Closed
wants to merge 16 commits into from
Closed

[Merged by Bors] - feat(linear_algebra/*): add lemma linear_independent.finite_of_is_noetherian #14714

wants to merge 16 commits into from

Commits on Jun 13, 2022

  1. feat(linear_algebra/*): add lemma `linear_independent.finite_of_is_no… 

    …etherian`

This replaces `fintype_of_is_noetherian_linear_independent` which gave the same
conclusion except demanded `strong_rank_condition R` instead of just `nontrivial R`.

Also some other minor gaps filled.
    @ocfnash
    ocfnash committed Jun 13, 2022
    Configuration menu
    Copy the full SHA
    d7702c9 View commit details
    Browse the repository at this point in the history

  2. Fix name collision. 

    These fixes are necessary because we have introduced the import
`data.finite.basic` in `order.compactly_generated` which is then
transitively exported.
    @ocfnash
    ocfnash committed Jun 13, 2022
    Configuration menu
    Copy the full SHA
    df18138 View commit details
    Browse the repository at this point in the history

  3. fix

    @ocfnash
    ocfnash committed Jun 13, 2022
    Configuration menu
    Copy the full SHA
    fdf18b4 View commit details
    Browse the repository at this point in the history

  4. fix

    @ocfnash
    ocfnash committed Jun 13, 2022
    Configuration menu
    Copy the full SHA
    cf865a9 View commit details
    Browse the repository at this point in the history

  5. fix

    @ocfnash
    ocfnash committed Jun 13, 2022
    Configuration menu
    Copy the full SHA
    b8a0bd6 View commit details
    Browse the repository at this point in the history

Commits on Jun 14, 2022

  1. merge master

    @ocfnash
    ocfnash committed Jun 14, 2022
    Configuration menu
    Copy the full SHA
    cc770d1 View commit details
    Browse the repository at this point in the history

Commits on Jun 22, 2022

  1. Fix spelling set_indepdent_range → set_independent_range

    @ocfnash
    ocfnash committed Jun 22, 2022
    Configuration menu
    Copy the full SHA
    a6169a8 View commit details
    Browse the repository at this point in the history

Commits on Jun 23, 2022

  1. Merge branch 'master' into ocfnash/linear_indep_finite

    @ocfnash
    ocfnash committed Jun 23, 2022
    Configuration menu
    Copy the full SHA
    40fe182 View commit details
    Browse the repository at this point in the history

  2. Use set.finite_of_finite instead of fintype.of_finite

    @ocfnash
    ocfnash committed Jun 23, 2022
    Configuration menu
    Copy the full SHA
    5b4494b View commit details
    Browse the repository at this point in the history

Commits on Jun 26, 2022

  1. Rename linear_independent.independent to `linear_independent.indepe… 

    …ndent_span_singleton`

Suggestion of CR
    @ocfnash
    ocfnash committed Jun 26, 2022
    Configuration menu
    Copy the full SHA
    a7183f2 View commit details
    Browse the repository at this point in the history

Commits on Jun 27, 2022

  1. Allow Prop indexing in complete_lattice.independent.comp(').

    @ocfnash
    ocfnash committed Jun 27, 2022
    Configuration menu
    Copy the full SHA
    b964728 View commit details
    Browse the repository at this point in the history

  2. Micro golfing

    @ocfnash
    ocfnash committed Jun 27, 2022
    Configuration menu
    Copy the full SHA
    25932f6 View commit details
    Browse the repository at this point in the history

  3. Add lemma finite.of_injective_finite_range to golf `complete_lattic… 

    …e.well_founded.finite_of_independent`
    @ocfnash
    ocfnash committed Jun 27, 2022
    Configuration menu
    Copy the full SHA
    7f153fa View commit details
    Browse the repository at this point in the history

  4. fix

    @ocfnash
    ocfnash committed Jun 27, 2022
    Configuration menu
    Copy the full SHA
    fa50bf7 View commit details
    Browse the repository at this point in the history

  5. fix (part 2)

    @ocfnash
    ocfnash committed Jun 27, 2022
    Configuration menu
    Copy the full SHA
    91679c1 View commit details
    Browse the repository at this point in the history

  6. Suggestions from CR

    @ocfnash
    ocfnash committed Jun 27, 2022
    Configuration menu
    Copy the full SHA
    d2f70c5 View commit details
    Browse the repository at this point in the history