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(data/fin): add some lemmas about coercions #2522

Closed
wants to merge 12 commits into from
Closed

[Merged by Bors] - feat(data/fin): add some lemmas about coercions #2522

wants to merge 12 commits into from

Commits on Apr 25, 2020

  1. feat(data/fin): add some lemmas about coercions and of_nat 

    Two of these lemmas allow norm_cast to work with inequalities
involving fin values converted to ℕ.  The rest are for simplifying
expressions where of_nat is used to convert from ℕ to fin, in cases
where an inequality means of_nat does not in fact change the value.

There are very few lemmas relating to of_nat in mathlib at present.
These lemmas were found useful in formalising solutions to an olympiad
problem, see
<https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Some.20olympiad.20formalisations>,
and seem more generally relevant than to just that particular problem.
    @jsm28
    jsm28 committed Apr 25, 2020
    Configuration menu
    Copy the full SHA
    9a1983f View commit details
    Browse the repository at this point in the history

  2. Use n + 1 in place of succ n.

    @jsm28
    jsm28 committed Apr 25, 2020
    Configuration menu
    Copy the full SHA
    2798d12 View commit details
    Browse the repository at this point in the history

  3. Update src/data/fin.lean 

    Co-Authored-By: Gabriel Ebner <gebner@gebner.org>
    @jsm28 @gebner
    jsm28 and gebner committed Apr 25, 2020
    Configuration menu
    Copy the full SHA
    398a933 View commit details
    Browse the repository at this point in the history

  4. Update src/data/fin.lean 

    Co-Authored-By: Gabriel Ebner <gebner@gebner.org>
    @jsm28 @gebner
    jsm28 and gebner committed Apr 25, 2020
    Configuration menu
    Copy the full SHA
    4db89e6 View commit details
    Browse the repository at this point in the history

  5. Update src/data/fin.lean 

    Co-Authored-By: Gabriel Ebner <gebner@gebner.org>
    @jsm28 @gebner
    jsm28 and gebner committed Apr 25, 2020
    Configuration menu
    Copy the full SHA
    e73c5eb View commit details
    Browse the repository at this point in the history

  6. Update src/data/fin.lean 

    Co-Authored-By: Gabriel Ebner <gebner@gebner.org>
    @jsm28 @gebner
    jsm28 and gebner committed Apr 25, 2020
    Configuration menu
    Copy the full SHA
    aca0480 View commit details
    Browse the repository at this point in the history

  7. Update src/data/fin.lean 

    Co-Authored-By: Gabriel Ebner <gebner@gebner.org>
    @jsm28 @gebner
    jsm28 and gebner committed Apr 25, 2020
    Configuration menu
    Copy the full SHA
    33fa042 View commit details
    Browse the repository at this point in the history

  8. Replace of_nat_coe_zero, add of_nat_one.

    @jsm28
    jsm28 committed Apr 25, 2020
    Configuration menu
    Copy the full SHA
    53336c2 View commit details
    Browse the repository at this point in the history

Commits on Apr 26, 2020

  1. Restate of_nat lemmas in terms of coercions instead, via of_nat_eq_coe.

    @jsm28
    jsm28 committed Apr 26, 2020
    Configuration menu
    Copy the full SHA
    b5c63ac View commit details
    Browse the repository at this point in the history

  2. Move more fin lemmas from data.zmod.basic to data.fin.

    @jsm28
    jsm28 committed Apr 26, 2020
    Configuration menu
    Copy the full SHA
    c9c57a0 View commit details
    Browse the repository at this point in the history

Commits on Apr 28, 2020

  1. Update src/data/nat/basic.lean 

    Co-Authored-By: Johan Commelin <johan@commelin.net>
    @jsm28 @jcommelin
    jsm28 and jcommelin committed Apr 28, 2020
    Configuration menu
    Copy the full SHA
    910a942 View commit details
    Browse the repository at this point in the history

  2. Also move mul_mod to data.nat.basic.

    @jsm28
    jsm28 committed Apr 28, 2020
    Configuration menu
    Copy the full SHA
    8ad163d View commit details
    Browse the repository at this point in the history