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

Hensel's lemma over the p-adic integers #337

Closed
wants to merge 29 commits into from
Closed

Hensel's lemma over the p-adic integers #337

wants to merge 29 commits into from

Commits on Sep 27, 2018

  1. feat(data/padics): use has_norm typeclasses for padics

    @robertylewis
    robertylewis committed Sep 27, 2018
    Configuration menu
    Copy the full SHA
    4f85f91 View commit details
    Browse the repository at this point in the history

  2. style(data/padic/padic_integers): remove comment, long line

    @robertylewis
    robertylewis committed Sep 27, 2018
    Configuration menu
    Copy the full SHA
    d9f1be1 View commit details
    Browse the repository at this point in the history

  3. feat(data/padics): more scattered lemmas, integers are complete

    @robertylewis
    robertylewis committed Sep 27, 2018
    Configuration menu
    Copy the full SHA
    ba27d2f View commit details
    Browse the repository at this point in the history

  4. feat(algebra): various helper lemmas, mostly about powers

    @robertylewis
    robertylewis committed Sep 27, 2018
    Configuration menu
    Copy the full SHA
    29f723f View commit details
    Browse the repository at this point in the history

  5. feat(data/real,analysis/limits): some properties about limits of sequ… 

    …ences
    @robertylewis
    robertylewis committed Sep 27, 2018
    Configuration menu
    Copy the full SHA
    7587fe2 View commit details
    Browse the repository at this point in the history

  6. feat(data/finsupp,data/polynomial): facts about polynomials

    @robertylewis
    robertylewis committed Sep 27, 2018
    Configuration menu
    Copy the full SHA
    73a0f0d View commit details
    Browse the repository at this point in the history

  7. feat(data/nat): helper lemmas

    @robertylewis
    robertylewis committed Sep 27, 2018
    Configuration menu
    Copy the full SHA
    237c23f View commit details
    Browse the repository at this point in the history

  8. feat(analysis/normed_space,analysis/topology/topological_structures):… 

    … helper lemmas
    @robertylewis
    robertylewis committed Sep 27, 2018
    Configuration menu
    Copy the full SHA
    1b8a2d9 View commit details
    Browse the repository at this point in the history

  9. feat(data/padics): prove Hensel's lemma

    @robertylewis
    robertylewis committed Sep 27, 2018
    Configuration menu
    Copy the full SHA
    cfad546 View commit details
    Browse the repository at this point in the history

  10. fix(analysis/normed_space,data/padics): fix mistake in merge; remove … 

    …dead file
    @robertylewis
    robertylewis committed Sep 27, 2018
    Configuration menu
    Copy the full SHA
    89fa0b7 View commit details
    Browse the repository at this point in the history

  11. fix(data/padics/hensel,data/real/cau_seq_filter): missing docstrings

    @robertylewis
    robertylewis committed Sep 27, 2018
    Configuration menu
    Copy the full SHA
    8e7399d View commit details
    Browse the repository at this point in the history

  12. feat(docs/theories): document padics development 

    (it hurts to write "maths in lean")
    @robertylewis
    robertylewis committed Sep 27, 2018
    Configuration menu
    Copy the full SHA
    124120f View commit details
    Browse the repository at this point in the history

  13. style(data/padics/hensel): polynomials and prime numbers have differe… 

    …nt names
    @robertylewis
    robertylewis committed Sep 27, 2018
    Configuration menu
    Copy the full SHA
    8184c0e View commit details
    Browse the repository at this point in the history

  14. feat(data/padics): address review comments

    @robertylewis
    robertylewis committed Sep 27, 2018
    Configuration menu
    Copy the full SHA
    a47b547 View commit details
    Browse the repository at this point in the history

  15. style(data/polynomial): variable name and comment

    @robertylewis
    robertylewis committed Sep 27, 2018
    Configuration menu
    Copy the full SHA
    82084f6 View commit details
    Browse the repository at this point in the history

  16. feat(data/padics): style, minor refactor

    @robertylewis
    robertylewis committed Sep 27, 2018
    Configuration menu
    Copy the full SHA
    713f3c6 View commit details
    Browse the repository at this point in the history

  17. feat(data/padics/padic_norm): add division lemma

    @robertylewis
    robertylewis committed Sep 27, 2018
    Configuration menu
    Copy the full SHA
    625f76e View commit details
    Browse the repository at this point in the history

  18. feat(data/padics/padic_norm): extra lemmas about padic val and norm

    @robertylewis
    robertylewis committed Sep 27, 2018
    Configuration menu
    Copy the full SHA
    c199015 View commit details
    Browse the repository at this point in the history

Commits on Sep 28, 2018

  1. feat(data/real/cau_seq): relate cauchy sequence completeness and filt… 

    …er completeness
    @robertylewis
    robertylewis committed Sep 28, 2018
    2 Configuration menu
    Copy the full SHA
    b72cc01 View commit details
    Browse the repository at this point in the history

Commits on Sep 29, 2018

  1. style(analysis/limits,data/real/cau_seq_filter): cleanup

    @robertylewis
    robertylewis committed Sep 29, 2018
    Configuration menu
    Copy the full SHA
    336b6c4 View commit details
    Browse the repository at this point in the history

Commits on Oct 1, 2018

  1. remove tactic.find

    @johoelzl
    johoelzl committed Oct 1, 2018
    Configuration menu
    Copy the full SHA
    db2c395 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into padic

    @johoelzl
    johoelzl committed Oct 1, 2018
    Configuration menu
    Copy the full SHA
    f37821c View commit details
    Browse the repository at this point in the history

Commits on Oct 2, 2018

  1. feat(data/padics): use prime typeclass

    @robertylewis
    robertylewis committed Oct 2, 2018
    Configuration menu
    Copy the full SHA
    4719d34 View commit details
    Browse the repository at this point in the history

  2. feat(data/real,data/padics): cauchy_complete typeclass

    @robertylewis
    robertylewis committed Oct 2, 2018
    Configuration menu
    Copy the full SHA
    54cbd88 View commit details
    Browse the repository at this point in the history

  3. fix(data/real,data/padics): remove dead code

    @robertylewis
    robertylewis committed Oct 2, 2018
    Configuration menu
    Copy the full SHA
    020924c View commit details
    Browse the repository at this point in the history

  4. style(data/padics): anonymous instances

    @robertylewis
    robertylewis committed Oct 2, 2018
    Configuration menu
    Copy the full SHA
    7bf76f2 View commit details
    Browse the repository at this point in the history

  5. fix(data/real,data/padics): fix merge

    @robertylewis
    robertylewis committed Oct 2, 2018
    Configuration menu
    Copy the full SHA
    01f18f6 View commit details
    Browse the repository at this point in the history

  6. refactor(data/polynomial): remove analysis import

    @robertylewis
    robertylewis committed Oct 2, 2018
    Configuration menu
    Copy the full SHA
    7a1398e View commit details
    Browse the repository at this point in the history

  7. style(analysis/polynomial): unnecessary dsimp

    @robertylewis
    robertylewis committed Oct 2, 2018
    Configuration menu
    Copy the full SHA
    9c168db View commit details
    Browse the repository at this point in the history