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

feat(number_theory/miller_rabin): adding lemmas about the miller rabin primality test. #12254

Open
wants to merge 304 commits into
base: master
Choose a base branch
from
Open

feat(number_theory/miller_rabin): adding lemmas about the miller rabin primality test. #12254

wants to merge 304 commits into from
This pull request is big! We’re only showing the most recent 250 commits.

Commits on Mar 17, 2022

  1. progress

    @seangolinski7
    seangolinski7 committed Mar 17, 2022
    Configuration menu
    Copy the full SHA
    847bbaf View commit details
    Browse the repository at this point in the history

Commits on Mar 18, 2022

  1. add new todos

    @BoltonBailey
    BoltonBailey committed Mar 18, 2022
    Configuration menu
    Copy the full SHA
    7076b57 View commit details
    Browse the repository at this point in the history

Commits on Mar 20, 2022

  1. new todos

    @BoltonBailey
    BoltonBailey committed Mar 20, 2022
    Configuration menu
    Copy the full SHA
    fe7ce5d View commit details
    Browse the repository at this point in the history

  2. progress

    @seangolinski7
    seangolinski7 committed Mar 20, 2022
    Configuration menu
    Copy the full SHA
    7f450ed View commit details
    Browse the repository at this point in the history

  3. Merge branch 'miller-rabin' of https://github.com/leanprover-communit… 

    …y/mathlib into miller-rabin
    @seangolinski7
    seangolinski7 committed Mar 20, 2022
    Configuration menu
    Copy the full SHA
    4c75751 View commit details
    Browse the repository at this point in the history

Commits on Mar 23, 2022

  1. mwe file

    @seangolinski7
    seangolinski7 committed Mar 23, 2022
    Configuration menu
    Copy the full SHA
    c664e5c View commit details
    Browse the repository at this point in the history

  2. changed mwe

    @BoltonBailey
    BoltonBailey committed Mar 23, 2022
    Configuration menu
    Copy the full SHA
    e913de5 View commit details
    Browse the repository at this point in the history

  3. git task

    @BoltonBailey
    BoltonBailey committed Mar 23, 2022
    Configuration menu
    Copy the full SHA
    424b22c View commit details
    Browse the repository at this point in the history

  4. refactor task

    @BoltonBailey
    BoltonBailey committed Mar 23, 2022
    Configuration menu
    Copy the full SHA
    e90e47b View commit details
    Browse the repository at this point in the history

Commits on Mar 27, 2022

  1. Changed recs

    @BoltonBailey
    BoltonBailey committed Mar 27, 2022
    Configuration menu
    Copy the full SHA
    d4bcbf3 View commit details
    Browse the repository at this point in the history

  2. typo

    @BoltonBailey
    BoltonBailey committed Mar 27, 2022
    Configuration menu
    Copy the full SHA
    1d373ed View commit details
    Browse the repository at this point in the history

  3. simp lemmas for succinctness

    @BoltonBailey
    BoltonBailey committed Mar 27, 2022
    Configuration menu
    Copy the full SHA
    03b3a70 View commit details
    Browse the repository at this point in the history

  4. golfing

    @BoltonBailey
    BoltonBailey committed Mar 27, 2022
    Configuration menu
    Copy the full SHA
    6dcc110 View commit details
    Browse the repository at this point in the history

  5. progress

    @seangolinski7
    seangolinski7 committed Mar 27, 2022
    Configuration menu
    Copy the full SHA
    94340ee View commit details
    Browse the repository at this point in the history

  6. fixed von_mangold_sum proof

    @seangolinski7
    seangolinski7 committed Mar 27, 2022
    Configuration menu
    Copy the full SHA
    b87c722 View commit details
    Browse the repository at this point in the history

  7. added gcd_mul_of_dvd_coprime

    @seangolinski7
    seangolinski7 committed Mar 27, 2022
    Configuration menu
    Copy the full SHA
    c2cc886 View commit details
    Browse the repository at this point in the history

  8. progress

    @seangolinski7
    seangolinski7 committed Mar 27, 2022
    Configuration menu
    Copy the full SHA
    2d603ba View commit details
    Browse the repository at this point in the history

  9. Merge branch 'master' of https://github.com/leanprover-community/mathlib 

     into miller-rabin
    @seangolinski7
    seangolinski7 committed Mar 27, 2022
    Configuration menu
    Copy the full SHA
    2266b49 View commit details
    Browse the repository at this point in the history

Commits on Mar 28, 2022

  1. Merge branch 'gcd_mul_of_dvd_coprime' of github.com:leanprover-commun… 

    …ity/mathlib into miller-rabin
    @BoltonBailey
    BoltonBailey committed Mar 28, 2022
    Configuration menu
    Copy the full SHA
    6510dc2 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'BoltonBailey/nat_rec_edits' of github.com:leanprover-co… 

    …mmunity/mathlib into miller-rabin
    @BoltonBailey
    BoltonBailey committed Mar 28, 2022
    Configuration menu
    Copy the full SHA
    ef6280a View commit details
    Browse the repository at this point in the history

  3. TODOs

    @BoltonBailey
    BoltonBailey committed Mar 28, 2022
    Configuration menu
    Copy the full SHA
    8ea067d View commit details
    Browse the repository at this point in the history

Commits on Mar 31, 2022

  1. progress

    @seangolinski7
    seangolinski7 committed Mar 31, 2022
    Configuration menu
    Copy the full SHA
    f9a1263 View commit details
    Browse the repository at this point in the history

  2. changes to gcd_mul_of_coprime_of_dvd name

    @seangolinski7
    seangolinski7 committed Mar 31, 2022
    Configuration menu
    Copy the full SHA
    7e9798a View commit details
    Browse the repository at this point in the history

  3. Update src/data/nat/gcd.lean 

    Co-authored-by: Johan Commelin <johan@commelin.net>
    @seangolinski7 @jcommelin
    seangolinski7 and jcommelin committed Mar 31, 2022
    Configuration menu
    Copy the full SHA
    9e65ce9 View commit details
    Browse the repository at this point in the history

  4. name change

    @seangolinski7
    seangolinski7 committed Mar 31, 2022
    Configuration menu
    Copy the full SHA
    58da701 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'gcd_mul_of_dvd_coprime' of https://github.com/leanprove… 

    …r-community/mathlib into miller-rabin
    @seangolinski7
    seangolinski7 committed Mar 31, 2022
    Configuration menu
    Copy the full SHA
    3484417 View commit details
    Browse the repository at this point in the history

Commits on Apr 2, 2022

  1. changes

    @BoltonBailey
    BoltonBailey committed Apr 2, 2022
    Configuration menu
    Copy the full SHA
    118195d View commit details
    Browse the repository at this point in the history

  2. Merge branch 'miller-rabin' of github.com:leanprover-community/mathli… 

    …b into miller-rabin
    @BoltonBailey
    BoltonBailey committed Apr 2, 2022
    Configuration menu
    Copy the full SHA
    55f541c View commit details
    Browse the repository at this point in the history

Commits on Apr 3, 2022

  1. progress

    @seangolinski7
    seangolinski7 committed Apr 3, 2022
    Configuration menu
    Copy the full SHA
    5434550 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'miller-rabin' of https://github.com/leanprover-communit… 

    …y/mathlib into miller-rabin
    @seangolinski7
    seangolinski7 committed Apr 3, 2022
    Configuration menu
    Copy the full SHA
    f344b9a View commit details
    Browse the repository at this point in the history

  3. new fast multiplicity def

    @BoltonBailey
    BoltonBailey committed Apr 3, 2022
    Configuration menu
    Copy the full SHA
    cd668ad View commit details
    Browse the repository at this point in the history

Commits on Apr 4, 2022

  1. add proper subgroup theorem

    @BoltonBailey
    BoltonBailey committed Apr 4, 2022
    Configuration menu
    Copy the full SHA
    352946a View commit details
    Browse the repository at this point in the history

  2. correct definition

    @BoltonBailey
    BoltonBailey committed Apr 4, 2022
    Configuration menu
    Copy the full SHA
    6892c4f View commit details
    Browse the repository at this point in the history

Commits on Apr 6, 2022

  1. progress

    @seangolinski7
    seangolinski7 committed Apr 6, 2022
    Configuration menu
    Copy the full SHA
    cc42836 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'miller-rabin' of https://github.com/leanprover-communit… 

    …y/mathlib into miller-rabin
    @seangolinski7
    seangolinski7 committed Apr 6, 2022
    Configuration menu
    Copy the full SHA
    c3d431e View commit details
    Browse the repository at this point in the history

  3. progress

    @seangolinski7
    seangolinski7 committed Apr 6, 2022
    Configuration menu
    Copy the full SHA
    93f6a90 View commit details
    Browse the repository at this point in the history

  4. resolved merge conflicts

    @seangolinski7
    seangolinski7 committed Apr 6, 2022
    Configuration menu
    Copy the full SHA
    52f9e49 View commit details
    Browse the repository at this point in the history

Commits on Apr 10, 2022

  1. resolved merge conflict

    @seangolinski7
    seangolinski7 committed Apr 10, 2022
    Configuration menu
    Copy the full SHA
    b4f7d16 View commit details
    Browse the repository at this point in the history

  2. add rw

    @BoltonBailey
    BoltonBailey committed Apr 10, 2022
    Configuration menu
    Copy the full SHA
    8956e68 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'miller-rabin' of github.com:leanprover-community/mathli… 

    …b into miller-rabin
    @BoltonBailey
    BoltonBailey committed Apr 10, 2022
    Configuration menu
    Copy the full SHA
    cc4db1a View commit details
    Browse the repository at this point in the history

  4. TODOs for Bolton lol

    @seangolinski7
    seangolinski7 committed Apr 10, 2022
    Configuration menu
    Copy the full SHA
    213e31b View commit details
    Browse the repository at this point in the history

Commits on Apr 11, 2022

  1. fixed hypothesis

    @BoltonBailey
    BoltonBailey committed Apr 11, 2022
    Configuration menu
    Copy the full SHA
    3fe90fc View commit details
    Browse the repository at this point in the history

Commits on Apr 13, 2022

  1. another todo

    @BoltonBailey
    BoltonBailey committed Apr 13, 2022
    Configuration menu
    Copy the full SHA
    e41d2f4 View commit details
    Browse the repository at this point in the history

  2. Delete mwe.lean

    @BoltonBailey
    BoltonBailey committed Apr 13, 2022
    Configuration menu
    Copy the full SHA
    c1fe337 View commit details
    Browse the repository at this point in the history

  3. solve goal

    @BoltonBailey
    BoltonBailey committed Apr 13, 2022
    Configuration menu
    Copy the full SHA
    6de264c View commit details
    Browse the repository at this point in the history

  4. Merge branch 'miller-rabin' of github.com:leanprover-community/mathli… 

    …b into miller-rabin
    @BoltonBailey
    BoltonBailey committed Apr 13, 2022
    Configuration menu
    Copy the full SHA
    be2385b View commit details
    Browse the repository at this point in the history

  5. progress

    @seangolinski7
    seangolinski7 committed Apr 13, 2022
    Configuration menu
    Copy the full SHA
    511c05b View commit details
    Browse the repository at this point in the history

  6. Merge branch 'miller-rabin' of https://github.com/leanprover-communit… 

    …y/mathlib into miller-rabin
    @seangolinski7
    seangolinski7 committed Apr 13, 2022
    Configuration menu
    Copy the full SHA
    f2c2c3b View commit details
    Browse the repository at this point in the history

  7. progress

    @seangolinski7
    seangolinski7 committed Apr 13, 2022
    Configuration menu
    Copy the full SHA
    c15a370 View commit details
    Browse the repository at this point in the history

  8. work

    @BoltonBailey
    BoltonBailey committed Apr 13, 2022
    Configuration menu
    Copy the full SHA
    f5434cb View commit details
    Browse the repository at this point in the history

  9. Merge branch 'miller-rabin' of github.com:leanprover-community/mathli… 

    …b into miller-rabin
    @BoltonBailey
    BoltonBailey committed Apr 13, 2022
    Configuration menu
    Copy the full SHA
    b169118 View commit details
    Browse the repository at this point in the history

Commits on Apr 14, 2022

  1. work on 1 case

    @BoltonBailey
    BoltonBailey committed Apr 14, 2022
    Configuration menu
    Copy the full SHA
    9c2b771 View commit details
    Browse the repository at this point in the history

Commits on Apr 15, 2022

  1. testing in progress

    @seangolinski7
    seangolinski7 committed Apr 15, 2022
    Configuration menu
    Copy the full SHA
    12b890b View commit details
    Browse the repository at this point in the history

  2. Merge branch 'miller-rabin' of https://github.com/leanprover-communit… 

    …y/mathlib into miller-rabin
    @seangolinski7
    seangolinski7 committed Apr 15, 2022
    Configuration menu
    Copy the full SHA
    91e4979 View commit details
    Browse the repository at this point in the history

Commits on Apr 16, 2022

  1. commit

    @BoltonBailey
    BoltonBailey committed Apr 16, 2022
    Configuration menu
    Copy the full SHA
    af09797 View commit details
    Browse the repository at this point in the history

Commits on Apr 17, 2022

  1. proofs

    @seangolinski7
    seangolinski7 committed Apr 17, 2022
    Configuration menu
    Copy the full SHA
    15bcea4 View commit details
    Browse the repository at this point in the history

  2. small change

    @seangolinski7
    seangolinski7 committed Apr 17, 2022
    Configuration menu
    Copy the full SHA
    8942d80 View commit details
    Browse the repository at this point in the history

  3. changes

    @BoltonBailey
    BoltonBailey committed Apr 17, 2022
    Configuration menu
    Copy the full SHA
    65534e3 View commit details
    Browse the repository at this point in the history

  4. changes

    @BoltonBailey
    BoltonBailey committed Apr 17, 2022
    Configuration menu
    Copy the full SHA
    b7656f5 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'miller-rabin' of github.com:leanprover-community/mathli… 

    …b into miller-rabin
    @BoltonBailey
    BoltonBailey committed Apr 17, 2022
    Configuration menu
    Copy the full SHA
    8aa54ef View commit details
    Browse the repository at this point in the history

  6. made fermat test work

    @BoltonBailey
    BoltonBailey committed Apr 17, 2022
    Configuration menu
    Copy the full SHA
    47681ed View commit details
    Browse the repository at this point in the history

  7. new tests

    @BoltonBailey
    BoltonBailey committed Apr 17, 2022
    Configuration menu
    Copy the full SHA
    92bc2cf View commit details
    Browse the repository at this point in the history

  8. new test

    @BoltonBailey
    BoltonBailey committed Apr 17, 2022
    Configuration menu
    Copy the full SHA
    39f296c View commit details
    Browse the repository at this point in the history

Commits on Apr 21, 2022

  1. fix card lemma

    @BoltonBailey
    BoltonBailey committed Apr 21, 2022
    Configuration menu
    Copy the full SHA
    d9f42b8 View commit details
    Browse the repository at this point in the history

  2. edits

    @BoltonBailey
    BoltonBailey committed Apr 21, 2022
    Configuration menu
    Copy the full SHA
    43893a2 View commit details
    Browse the repository at this point in the history

Commits on Apr 22, 2022

  1. progress

    @BoltonBailey
    BoltonBailey committed Apr 22, 2022
    Configuration menu
    Copy the full SHA
    a712019 View commit details
    Browse the repository at this point in the history

Commits on Jul 20, 2022

  1. Define padic_part and p_odd_part

    @stuart-presnell
    stuart-presnell committed Jul 20, 2022
    Configuration menu
    Copy the full SHA
    ccf9237 View commit details
    Browse the repository at this point in the history

  2. Add padic_part_def and p_odd_part_def

    @stuart-presnell
    stuart-presnell committed Jul 20, 2022
    Configuration menu
    Copy the full SHA
    df37af5 View commit details
    Browse the repository at this point in the history

  3. Move pow_factorization_dvd

    @stuart-presnell
    stuart-presnell committed Jul 20, 2022
    Configuration menu
    Copy the full SHA
    6abeb94 View commit details
    Browse the repository at this point in the history

  4. Edit pow_factorization_dvd

    @stuart-presnell
    stuart-presnell committed Jul 20, 2022
    Configuration menu
    Copy the full SHA
    beba86e View commit details
    Browse the repository at this point in the history

  5. Move and edit pow_factorization_le

    @stuart-presnell
    stuart-presnell committed Jul 20, 2022
    Configuration menu
    Copy the full SHA
    4c59722 View commit details
    Browse the repository at this point in the history

  6. Move and edit div_pow_factorization_ne_zero

    @stuart-presnell
    stuart-presnell committed Jul 20, 2022
    Configuration menu
    Copy the full SHA
    34fcc20 View commit details
    Browse the repository at this point in the history

  7. Add TODO

    @stuart-presnell
    stuart-presnell committed Jul 20, 2022
    Configuration menu
    Copy the full SHA
    49a16e5 View commit details
    Browse the repository at this point in the history

  8. Move lemmas back

    @stuart-presnell
    stuart-presnell committed Jul 20, 2022
    Configuration menu
    Copy the full SHA
    3acab4d View commit details
    Browse the repository at this point in the history

  9. Add lemma padic_part_ne_zero

    @stuart-presnell
    stuart-presnell committed Jul 20, 2022
    Configuration menu
    Copy the full SHA
    3dfa764 View commit details
    Browse the repository at this point in the history

  10. Rename to padic_part_pos and padic_part_le

    @stuart-presnell
    stuart-presnell committed Jul 20, 2022
    Configuration menu
    Copy the full SHA
    a37db57 View commit details
    Browse the repository at this point in the history

  11. Add TODOs

    @stuart-presnell
    stuart-presnell committed Jul 20, 2022
    Configuration menu
    Copy the full SHA
    7d895e8 View commit details
    Browse the repository at this point in the history

  12. Rename div_pow_factorization_ne_zero to p_odd_part

    @stuart-presnell
    stuart-presnell committed Jul 20, 2022
    Configuration menu
    Copy the full SHA
    6fedd45 View commit details
    Browse the repository at this point in the history

  13. Add p_odd_part_le

    @stuart-presnell
    stuart-presnell committed Jul 20, 2022
    Configuration menu
    Copy the full SHA
    f2e1e82 View commit details
    Browse the repository at this point in the history

  14. Add p_odd_part_dvd

    @stuart-presnell
    stuart-presnell committed Jul 20, 2022
    Configuration menu
    Copy the full SHA
    ffac414 View commit details
    Browse the repository at this point in the history

  15. Move & edit not_dvd_div_pow_factorization

    @stuart-presnell
    stuart-presnell committed Jul 20, 2022
    Configuration menu
    Copy the full SHA
    9197944 View commit details
    Browse the repository at this point in the history

  16. Prove padic_mul_p_odd_part_eq_self

    @stuart-presnell
    stuart-presnell committed Jul 20, 2022
    Configuration menu
    Copy the full SHA
    3844701 View commit details
    Browse the repository at this point in the history

  17. Prove mul_padic_part

    @stuart-presnell
    stuart-presnell committed Jul 20, 2022
    Configuration menu
    Copy the full SHA
    b8379d6 View commit details
    Browse the repository at this point in the history

  18. Prove mul_p_odd_part

    @stuart-presnell
    stuart-presnell committed Jul 20, 2022
    Configuration menu
    Copy the full SHA
    df0c5ca View commit details
    Browse the repository at this point in the history

  19. Edit pow_dvd_iff_dvd_pow_factorization

    @stuart-presnell
    stuart-presnell committed Jul 20, 2022
    Configuration menu
    Copy the full SHA
    1afd8af View commit details
    Browse the repository at this point in the history

  20. Fix TODO!

    @stuart-presnell
    stuart-presnell committed Jul 20, 2022
    Configuration menu
    Copy the full SHA
    7bdfd52 View commit details
    Browse the repository at this point in the history

  21. Prove factorization_p_odd_part

    @stuart-presnell
    stuart-presnell committed Jul 20, 2022
    Configuration menu
    Copy the full SHA
    33ff397 View commit details
    Browse the repository at this point in the history

Commits on Jul 21, 2022

  1. Merge branch 'master' into SP_padic_odd_part

    @stuart-presnell
    stuart-presnell committed Jul 21, 2022
    Configuration menu
    Copy the full SHA
    5f38419 View commit details
    Browse the repository at this point in the history

  2. Delete noncomputable :)

    @stuart-presnell
    stuart-presnell committed Jul 21, 2022
    Configuration menu
    Copy the full SHA
    3a8d8e3 View commit details
    Browse the repository at this point in the history

  3. Fix docstring!

    @stuart-presnell
    stuart-presnell committed Jul 21, 2022
    Configuration menu
    Copy the full SHA
    0cd8cad View commit details
    Browse the repository at this point in the history

  4. Prove dvd_p_odd_part_of_dvd_not_dvd

    @stuart-presnell
    stuart-presnell committed Jul 21, 2022
    Configuration menu
    Copy the full SHA
    c02969e View commit details
    Browse the repository at this point in the history

  5. Rename & edit coprime_of_p_odd_part

    @stuart-presnell
    stuart-presnell committed Jul 21, 2022
    Configuration menu
    Copy the full SHA
    4a6d78c View commit details
    Browse the repository at this point in the history

  6. Update TODO list

    @stuart-presnell
    stuart-presnell committed Jul 21, 2022
    Configuration menu
    Copy the full SHA
    cf99d54 View commit details
    Browse the repository at this point in the history

  7. Add dvd_padic_part_of_dvd

    @stuart-presnell
    stuart-presnell committed Jul 21, 2022
    Configuration menu
    Copy the full SHA
    60e9700 View commit details
    Browse the repository at this point in the history

  8. Temp: add eq_of_dvd_div_eq_one

    @stuart-presnell
    stuart-presnell committed Jul 21, 2022
    Configuration menu
    Copy the full SHA
    5d53981 View commit details
    Browse the repository at this point in the history

  9. Add is_prime_pow_of_p_odd_part_eq_one

    @stuart-presnell
    stuart-presnell committed Jul 21, 2022
    Configuration menu
    Copy the full SHA
    351caae View commit details
    Browse the repository at this point in the history

  10. Fix is_prime_pow_iff_unique_prime_dvd

    @stuart-presnell
    stuart-presnell committed Jul 21, 2022
    Configuration menu
    Copy the full SHA
    e01a328 View commit details
    Browse the repository at this point in the history

  11. Add lemmas for ¬ p.prime

    @stuart-presnell
    stuart-presnell committed Jul 21, 2022
    Configuration menu
    Copy the full SHA
    5cb97a7 View commit details
    Browse the repository at this point in the history

  12. Remove @simp to fix lint; fix proofs

    @stuart-presnell
    stuart-presnell committed Jul 21, 2022
    Configuration menu
    Copy the full SHA
    ccfdc27 View commit details
    Browse the repository at this point in the history

Commits on Jul 22, 2022

  1. Test: reducible

    @stuart-presnell
    stuart-presnell committed Jul 22, 2022
    Configuration menu
    Copy the full SHA
    8469358 View commit details
    Browse the repository at this point in the history

Commits on Jul 23, 2022

  1. Change notation to ord[p] and coord[p]

    @stuart-presnell
    stuart-presnell committed Jul 23, 2022
    Configuration menu
    Copy the full SHA
    bf59733 View commit details
    Browse the repository at this point in the history

  2. Fix factorization/prime_pow

    @stuart-presnell
    stuart-presnell committed Jul 23, 2022
    Configuration menu
    Copy the full SHA
    8b9f88d View commit details
    Browse the repository at this point in the history

  3. Use ord in definition of coord

    @stuart-presnell
    stuart-presnell committed Jul 23, 2022
    Configuration menu
    Copy the full SHA
    ed189c8 View commit details
    Browse the repository at this point in the history

  4. delete #lint

    @stuart-presnell
    stuart-presnell committed Jul 23, 2022
    Configuration menu
    Copy the full SHA
    4309129 View commit details
    Browse the repository at this point in the history

Commits on Jul 25, 2022

  1. Rename to ord_proj and ord_compl

    @stuart-presnell
    stuart-presnell committed Jul 25, 2022
    Configuration menu
    Copy the full SHA
    e4e44b4 View commit details
    Browse the repository at this point in the history

  2. Rename lemmas

    @stuart-presnell
    stuart-presnell committed Jul 25, 2022
    Configuration menu
    Copy the full SHA
    6de7264 View commit details
    Browse the repository at this point in the history

  3. Swap in mul_ord_compl

    @stuart-presnell
    stuart-presnell committed Jul 25, 2022
    Configuration menu
    Copy the full SHA
    ca78de5 View commit details
    Browse the repository at this point in the history

  4. Rename to not_dvd_ord_compl

    @stuart-presnell
    stuart-presnell committed Jul 25, 2022
    Configuration menu
    Copy the full SHA
    e9bf18c View commit details
    Browse the repository at this point in the history

  5. Fix docstring

    @stuart-presnell
    stuart-presnell committed Jul 25, 2022
    Configuration menu
    Copy the full SHA
    3dd2314 View commit details
    Browse the repository at this point in the history

  6. Add new section header

    @stuart-presnell
    stuart-presnell committed Jul 25, 2022
    Configuration menu
    Copy the full SHA
    6f3be91 View commit details
    Browse the repository at this point in the history

  7. Revert unrelated changes to be PRed elsewhere

    @stuart-presnell
    stuart-presnell committed Jul 25, 2022
    Configuration menu
    Copy the full SHA
    7fcb8bd View commit details
    Browse the repository at this point in the history

Commits on Jul 26, 2022

  1. Change docstrings

    @stuart-presnell
    stuart-presnell committed Jul 26, 2022
    Configuration menu
    Copy the full SHA
    ae01773 View commit details
    Browse the repository at this point in the history

Commits on Jul 27, 2022

  1. Fix typo

    @stuart-presnell
    stuart-presnell committed Jul 27, 2022
    Configuration menu
    Copy the full SHA
    1e0528a View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into miller-rabin 

    Using computable `factorization`
    @stuart-presnell
    stuart-presnell committed Jul 27, 2022
    Configuration menu
    Copy the full SHA
    45579f7 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'SP_padic_odd_part' into miller-rabin 

    Using `ord_proj[2]` and `ord_compl[2]`
    @stuart-presnell
    stuart-presnell committed Jul 27, 2022
    Configuration menu
    Copy the full SHA
    a82de19 View commit details
    Browse the repository at this point in the history

  4. open nat

    @stuart-presnell
    stuart-presnell committed Jul 27, 2022
    Configuration menu
    Copy the full SHA
    0af5496 View commit details
    Browse the repository at this point in the history

Commits on Jul 28, 2022

  1. Fix some fails

    @stuart-presnell
    stuart-presnell committed Jul 28, 2022
    Configuration menu
    Copy the full SHA
    be1ad67 View commit details
    Browse the repository at this point in the history

  2. Add fintype.of_subgroup

    @stuart-presnell
    stuart-presnell committed Jul 28, 2022
    Configuration menu
    Copy the full SHA
    191a284 View commit details
    Browse the repository at this point in the history

  3. Fix another fail, comment out a rw

    @stuart-presnell
    stuart-presnell committed Jul 28, 2022
    Configuration menu
    Copy the full SHA
    e9af1f2 View commit details
    Browse the repository at this point in the history

  4. Format brackets

    @stuart-presnell
    stuart-presnell committed Jul 28, 2022
    Configuration menu
    Copy the full SHA
    e8617ee View commit details
    Browse the repository at this point in the history

  5. Add copyright notice

    @stuart-presnell
    stuart-presnell committed Jul 28, 2022
    Configuration menu
    Copy the full SHA
    4b2766f View commit details
    Browse the repository at this point in the history

  6. Fix overlong lines

    @stuart-presnell
    stuart-presnell committed Jul 28, 2022
    Configuration menu
    Copy the full SHA
    88ec692 View commit details
    Browse the repository at this point in the history

  7. Add temp docstring placeholders

    @stuart-presnell
    stuart-presnell committed Jul 28, 2022
    Configuration menu
    Copy the full SHA
    951ab25 View commit details
    Browse the repository at this point in the history

  8. Fix overlong lines

    @stuart-presnell
    stuart-presnell committed Jul 28, 2022
    Configuration menu
    Copy the full SHA
    a4e5ec1 View commit details
    Browse the repository at this point in the history

  9. Add temp docstring

    @stuart-presnell
    stuart-presnell committed Jul 28, 2022
    Configuration menu
    Copy the full SHA
    41df7d6 View commit details
    Browse the repository at this point in the history

  10. Add temp docstring

    @stuart-presnell
    stuart-presnell committed Jul 28, 2022
    Configuration menu
    Copy the full SHA
    7899b95 View commit details
    Browse the repository at this point in the history

  11. Properly format temp docstrings

    @stuart-presnell
    stuart-presnell committed Jul 28, 2022
    Configuration menu
    Copy the full SHA
    e23746d View commit details
    Browse the repository at this point in the history

  12. Comment out set_option profiler true

    @stuart-presnell
    stuart-presnell committed Jul 28, 2022
    Configuration menu
    Copy the full SHA
    860e3fa View commit details
    Browse the repository at this point in the history

  13. Format bracket

    @stuart-presnell
    stuart-presnell committed Jul 28, 2022
    Configuration menu
    Copy the full SHA
    c37acf9 View commit details
    Browse the repository at this point in the history

  14. Move up imports

    @stuart-presnell
    stuart-presnell committed Jul 28, 2022
    Configuration menu
    Copy the full SHA
    3c67ee2 View commit details
    Browse the repository at this point in the history

  15. Comment out #eval; add trivial example

    @stuart-presnell
    stuart-presnell committed Jul 28, 2022
    Configuration menu
    Copy the full SHA
    d0caa65 View commit details
    Browse the repository at this point in the history

  16. Change padic_val_nat to factorization

    @stuart-presnell
    stuart-presnell committed Jul 28, 2022
    Configuration menu
    Copy the full SHA
    2af14bb View commit details
    Browse the repository at this point in the history

  17. Change "two_power" to "even"

    @stuart-presnell
    stuart-presnell committed Jul 28, 2022
    Configuration menu
    Copy the full SHA
    4f54ead View commit details
    Browse the repository at this point in the history

  18. docstring for strong_probable_prime

    @stuart-presnell
    stuart-presnell committed Jul 28, 2022
    Configuration menu
    Copy the full SHA
    605e356 View commit details
    Browse the repository at this point in the history

  19. Move up square_roots_of_one

    @stuart-presnell
    stuart-presnell committed Jul 28, 2022
    Configuration menu
    Copy the full SHA
    cdb668f View commit details
    Browse the repository at this point in the history

  20. Format square_roots_of_one

    @stuart-presnell
    stuart-presnell committed Jul 28, 2022
    Configuration menu
    Copy the full SHA
    de0865b View commit details
    Browse the repository at this point in the history

  21. Golf square_roots_of_one

    @stuart-presnell
    stuart-presnell committed Jul 28, 2022
    Configuration menu
    Copy the full SHA
    729cb47 View commit details
    Browse the repository at this point in the history

  22. Move down fermat_pseudoprime

    @stuart-presnell
    stuart-presnell committed Jul 28, 2022
    Configuration menu
    Copy the full SHA
    59c6162 View commit details
    Browse the repository at this point in the history

  23. docstring for repeated_halving_of_exponent

    @stuart-presnell
    stuart-presnell committed Jul 28, 2022
    Configuration menu
    Copy the full SHA
    bf61822 View commit details
    Browse the repository at this point in the history

  24. Golf repeated_halving_of_exponent

    @stuart-presnell
    stuart-presnell committed Jul 28, 2022
    Configuration menu
    Copy the full SHA
    189c734 View commit details
    Browse the repository at this point in the history

  25. Implicit args in repeated_halving_of_exponent

    @stuart-presnell
    stuart-presnell committed Jul 28, 2022
    Configuration menu
    Copy the full SHA
    25a9041 View commit details
    Browse the repository at this point in the history

  26. docstring for strong_probable_prime_of_prime

    @stuart-presnell
    stuart-presnell committed Jul 28, 2022
    Configuration menu
    Copy the full SHA
    7ef0cd4 View commit details
    Browse the repository at this point in the history

  27. Golf nat.even_two_pow_iff

    @stuart-presnell
    stuart-presnell committed Jul 28, 2022
    Configuration menu
    Copy the full SHA
    fe6f242 View commit details
    Browse the repository at this point in the history

  28. Move up nat.even_two_pow_iff

    @stuart-presnell
    stuart-presnell committed Jul 28, 2022
    Configuration menu
    Copy the full SHA
    907cefc View commit details
    Browse the repository at this point in the history

  29. docstrings for fermat_pseudoprime

    @stuart-presnell
    stuart-presnell committed Jul 28, 2022
    Configuration menu
    Copy the full SHA
    c3ce282 View commit details
    Browse the repository at this point in the history

  30. Golf fermat_..._probable_prime

    @stuart-presnell
    stuart-presnell committed Jul 28, 2022
    Configuration menu
    Copy the full SHA
    e6f174d View commit details
    Browse the repository at this point in the history

  31. Golf fermat_..._prime

    @stuart-presnell
    stuart-presnell committed Jul 28, 2022
    Configuration menu
    Copy the full SHA
    2374207 View commit details
    Browse the repository at this point in the history

  32. Move up sub_one_dvd_pow_sub_one

    @stuart-presnell
    stuart-presnell committed Jul 28, 2022
    Configuration menu
    Copy the full SHA
    d9840e6 View commit details
    Browse the repository at this point in the history

  33. Golf sub_one_dvd_pow_sub_one

    @stuart-presnell
    stuart-presnell committed Jul 28, 2022
    Configuration menu
    Copy the full SHA
    b1fc8bf View commit details
    Browse the repository at this point in the history

  34. Move and golf coprime_add_one

    @stuart-presnell
    stuart-presnell committed Jul 28, 2022
    Configuration menu
    Copy the full SHA
    fbb3ce8 View commit details
    Browse the repository at this point in the history

  35. Move and golf coprime_self_sub_one

    @stuart-presnell
    stuart-presnell committed Jul 28, 2022
    Configuration menu
    Copy the full SHA
    e58b3bb View commit details
    Browse the repository at this point in the history

Commits on Jul 29, 2022

  1. Start work on Theorem 3.4

    @stuart-presnell
    stuart-presnell committed Jul 29, 2022
    Configuration menu
    Copy the full SHA
    c7ad258 View commit details
    Browse the repository at this point in the history

  2. Prove factorization on p. 1 of Conrad

    @stuart-presnell
    stuart-presnell committed Jul 29, 2022
    Configuration menu
    Copy the full SHA
    c03ad1d View commit details
    Browse the repository at this point in the history

  3. Remove assumptions on polynomial factorization

    @stuart-presnell
    stuart-presnell committed Jul 29, 2022
    Configuration menu
    Copy the full SHA
    1847e57 View commit details
    Browse the repository at this point in the history

  4. Docstring for file explaining Miller-Rabin test

    @stuart-presnell
    stuart-presnell committed Jul 29, 2022
    Configuration menu
    Copy the full SHA
    3b25ff5 View commit details
    Browse the repository at this point in the history

  5. Generalise to factorise_pow_two_pow_sub_one

    @stuart-presnell
    stuart-presnell committed Jul 29, 2022
    Configuration menu
    Copy the full SHA
    9b2f259 View commit details
    Browse the repository at this point in the history

  6. Define miller_rabin_witness

    @stuart-presnell
    stuart-presnell committed Jul 29, 2022
    Configuration menu
    Copy the full SHA
    a6a7a62 View commit details
    Browse the repository at this point in the history

  7. Prove one_not_miller_rabin_witness

    @stuart-presnell
    stuart-presnell committed Jul 29, 2022
    Configuration menu
    Copy the full SHA
    bdce481 View commit details
    Browse the repository at this point in the history

  8. Prove minus_one_not_miller_rabin_witness

    @stuart-presnell
    stuart-presnell committed Jul 29, 2022
    Configuration menu
    Copy the full SHA
    1e18183 View commit details
    Browse the repository at this point in the history

  9. Prove odd_of_odd_part

    @stuart-presnell
    stuart-presnell committed Jul 29, 2022
    Configuration menu
    Copy the full SHA
    0f7e7b7 View commit details
    Browse the repository at this point in the history

  10. Fix minus_one_not_miller_rabin_witness

    @stuart-presnell
    stuart-presnell committed Jul 29, 2022
    Configuration menu
    Copy the full SHA
    dc9037a View commit details
    Browse the repository at this point in the history

  11. Edit definition of miller_rabin_witness

    @stuart-presnell
    stuart-presnell committed Jul 29, 2022
    Configuration menu
    Copy the full SHA
    394b187 View commit details
    Browse the repository at this point in the history

  12. Edit docstring for strong_probable_prime; prove

    @stuart-presnell
    stuart-presnell committed Jul 29, 2022
    Configuration menu
    Copy the full SHA
    bd88309 View commit details
    Browse the repository at this point in the history

  13. Define miller_rabin_sequence & eval examples

    @stuart-presnell
    stuart-presnell committed Jul 29, 2022
    Configuration menu
    Copy the full SHA
    7a8d1a7 View commit details
    Browse the repository at this point in the history

  14. Prove length_miller_rabin_sequence

    @stuart-presnell
    stuart-presnell committed Jul 29, 2022
    Configuration menu
    Copy the full SHA
    aec59ca View commit details
    Browse the repository at this point in the history

  15. Name strong_probable_prime_iff_nonwitness

    @stuart-presnell
    stuart-presnell committed Jul 29, 2022
    Configuration menu
    Copy the full SHA
    9146249 View commit details
    Browse the repository at this point in the history

  16. Prove strong_..._iff_miller_rabin_sequence

    @stuart-presnell
    stuart-presnell committed Jul 29, 2022
    Configuration menu
    Copy the full SHA
    1803884 View commit details
    Browse the repository at this point in the history

Commits on Jul 30, 2022

  1. Delete import number_theory.padics.padic_norm

    @stuart-presnell
    stuart-presnell committed Jul 30, 2022
    Configuration menu
    Copy the full SHA
    ebd69ed View commit details
    Browse the repository at this point in the history

  2. docstrings for even_part and odd_part

    @stuart-presnell
    stuart-presnell committed Jul 30, 2022
    Configuration menu
    Copy the full SHA
    558827e View commit details
    Browse the repository at this point in the history

  3. Prove factorization_two_pos_of_even_of_pos

    @stuart-presnell
    stuart-presnell committed Jul 30, 2022
    Configuration menu
    Copy the full SHA
    6bfffab View commit details
    Browse the repository at this point in the history

  4. Move down ±1 not witness

    @stuart-presnell
    stuart-presnell committed Jul 30, 2022
    Configuration menu
    Copy the full SHA
    da6c69c View commit details
    Browse the repository at this point in the history

  5. Add nat.mem_miller_rabin_sequence

    @stuart-presnell
    stuart-presnell committed Jul 30, 2022
    Configuration menu
    Copy the full SHA
    d940243 View commit details
    Browse the repository at this point in the history

  6. Golf minus_one_not_miller_rabin_witness

    @stuart-presnell
    stuart-presnell committed Jul 30, 2022
    Configuration menu
    Copy the full SHA
    a2ca8a3 View commit details
    Browse the repository at this point in the history

  7. Rename to factorization_two_pos_sub_one

    @stuart-presnell
    stuart-presnell committed Jul 30, 2022
    Configuration menu
    Copy the full SHA
    179ba00 View commit details
    Browse the repository at this point in the history

  8. Prove strong_probable_prime_of_prime'

    @stuart-presnell
    stuart-presnell committed Jul 30, 2022
    Configuration menu
    Copy the full SHA
    c76e06d View commit details
    Browse the repository at this point in the history

  9. Temporary name: factorize_poly

    @stuart-presnell
    stuart-presnell committed Jul 30, 2022
    Configuration menu
    Copy the full SHA
    2b39f44 View commit details
    Browse the repository at this point in the history

Commits on Jul 31, 2022

  1. Prove factorize_poly' for arbitrary comm_ring

    @stuart-presnell
    stuart-presnell committed Jul 31, 2022
    Configuration menu
    Copy the full SHA
    3e296dc View commit details
    Browse the repository at this point in the history

  2. strong_probable_prime_of_prime'' for zmod p

    @stuart-presnell
    stuart-presnell committed Jul 31, 2022
    Configuration menu
    Copy the full SHA
    a497f3d View commit details
    Browse the repository at this point in the history

  3. Move up strong_probable_prime_of_prime''

    @stuart-presnell
    stuart-presnell committed Jul 31, 2022
    Configuration menu
    Copy the full SHA
    cb8e3d7 View commit details
    Browse the repository at this point in the history

  4. Add section headers

    @stuart-presnell
    stuart-presnell committed Jul 31, 2022
    Configuration menu
    Copy the full SHA
    a5f93ec View commit details
    Browse the repository at this point in the history

  5. Rename Theorem 3.4

    @stuart-presnell
    stuart-presnell committed Jul 31, 2022
    Configuration menu
    Copy the full SHA
    4aa125c View commit details
    Browse the repository at this point in the history

  6. Define Fermat witness and Fermat candidate-prime

    @stuart-presnell
    stuart-presnell committed Jul 31, 2022
    Configuration menu
    Copy the full SHA
    2031937 View commit details
    Browse the repository at this point in the history

  7. Prove miller_rabin_witness_of_fermat_witness

    @stuart-presnell
    stuart-presnell committed Jul 31, 2022
    Configuration menu
    Copy the full SHA
    e2b58df View commit details
    Browse the repository at this point in the history

  8. Golf fermat_cprime_of_strong_probable_prime

    @stuart-presnell
    stuart-presnell committed Jul 31, 2022
    Configuration menu
    Copy the full SHA
    aa45646 View commit details
    Browse the repository at this point in the history

  9. Golf strong_probable_prime_of_prime_power_iff

    @stuart-presnell
    stuart-presnell committed Jul 31, 2022
    Configuration menu
    Copy the full SHA
    6de9ec5 View commit details
    Browse the repository at this point in the history

  10. open_locale nat to use φ for nat.totient

    @stuart-presnell
    stuart-presnell committed Jul 31, 2022
    Configuration menu
    Copy the full SHA
    defb221 View commit details
    Browse the repository at this point in the history

  11. Golf euler

    @stuart-presnell
    stuart-presnell committed Jul 31, 2022
    Configuration menu
    Copy the full SHA
    7770439 View commit details
    Browse the repository at this point in the history

  12. Golf by fermat_cprime_of_strong_probable_prime

    @stuart-presnell
    stuart-presnell committed Jul 31, 2022
    Configuration menu
    Copy the full SHA
    a01fe4c View commit details
    Browse the repository at this point in the history

  13. Golf 1st half of Theorem 3.4

    @stuart-presnell
    stuart-presnell committed Jul 31, 2022
    Configuration menu
    Copy the full SHA
    e88c107 View commit details
    Browse the repository at this point in the history

  14. Start 2nd half of Theorem 3.4

    @stuart-presnell
    stuart-presnell committed Jul 31, 2022
    Configuration menu
    Copy the full SHA
    c6a50cb View commit details
    Browse the repository at this point in the history

  15. Golf j=0 case

    @stuart-presnell
    stuart-presnell committed Jul 31, 2022
    Configuration menu
    Copy the full SHA
    2cff2b1 View commit details
    Browse the repository at this point in the history

  16. Structure of (j ≠ 0) case

    @stuart-presnell
    stuart-presnell committed Jul 31, 2022
    Configuration menu
    Copy the full SHA
    def57e0 View commit details
    Browse the repository at this point in the history

  17. Fill in hk_odd

    @stuart-presnell
    stuart-presnell committed Jul 31, 2022
    Configuration menu
    Copy the full SHA
    f51f26a View commit details
    Browse the repository at this point in the history

  18. Fill in hfe

    @stuart-presnell
    stuart-presnell committed Jul 31, 2022
    Configuration menu
    Copy the full SHA
    2f96f7d View commit details
    Browse the repository at this point in the history

  19. Fill in hx1

    @stuart-presnell
    stuart-presnell committed Jul 31, 2022
    Configuration menu
    Copy the full SHA
    58cf591 View commit details
    Browse the repository at this point in the history

  20. Clumsy draft of hx2

    @stuart-presnell
    stuart-presnell committed Jul 31, 2022
    Configuration menu
    Copy the full SHA
    d801317 View commit details
    Browse the repository at this point in the history

  21. Fill in h6

    @stuart-presnell
    stuart-presnell committed Jul 31, 2022
    Configuration menu
    Copy the full SHA
    81f1c3c View commit details
    Browse the repository at this point in the history

  22. Found an error in my write-up

    @stuart-presnell
    stuart-presnell committed Jul 31, 2022
    Configuration menu
    Copy the full SHA
    dc68987 View commit details
    Browse the repository at this point in the history

Commits on Aug 1, 2022

  1. Remove hα : 1 ≤ α

    @stuart-presnell
    stuart-presnell committed Aug 1, 2022
    Configuration menu
    Copy the full SHA
    6fab088 View commit details
    Browse the repository at this point in the history

  2. Add temp lemmas from #15793

    @stuart-presnell
    stuart-presnell committed Aug 1, 2022
    Configuration menu
    Copy the full SHA
    15f903c View commit details
    Browse the repository at this point in the history

  3. Finish hlk with ord_compl_dvd_ord_compl_of_dvd

    @stuart-presnell
    stuart-presnell committed Aug 1, 2022
    Configuration menu
    Copy the full SHA
    9768e28 View commit details
    Browse the repository at this point in the history

  4. Some minor edits

    @stuart-presnell
    stuart-presnell committed Aug 1, 2022
    Configuration menu
    Copy the full SHA
    24dc58f View commit details
    Browse the repository at this point in the history

  5. Add comments; rename H to hjf

    @stuart-presnell
    stuart-presnell committed Aug 1, 2022
    Configuration menu
    Copy the full SHA
    c55803d View commit details
    Browse the repository at this point in the history

  6. Introduce new hx1', hx2' to fix error; fill in h3

    @stuart-presnell
    stuart-presnell committed Aug 1, 2022
    Configuration menu
    Copy the full SHA
    463467d View commit details
    Browse the repository at this point in the history

  7. Re-write proof structure to fix earlier big error

    @stuart-presnell
    stuart-presnell committed Aug 1, 2022
    Configuration menu
    Copy the full SHA
    4b2908b View commit details
    Browse the repository at this point in the history

  8. Move exponents

    @stuart-presnell
    stuart-presnell committed Aug 1, 2022
    Configuration menu
    Copy the full SHA
    d0137d1 View commit details
    Browse the repository at this point in the history

Commits on Aug 2, 2022

  1. Factor spp_of_prime_power_iff thru square_roots_of_one

    @stuart-presnell
    stuart-presnell committed Aug 2, 2022
    Configuration menu
    Copy the full SHA
    cc5bdaf View commit details
    Browse the repository at this point in the history

  2. Prove square_roots_of_one for x : ℕ

    @stuart-presnell
    stuart-presnell committed Aug 2, 2022
    Configuration menu
    Copy the full SHA
    e84fbe6 View commit details
    Browse the repository at this point in the history

  3. Outline of square_roots_of_one for zmod (p^α)

    @stuart-presnell
    stuart-presnell committed Aug 2, 2022
    Configuration menu
    Copy the full SHA
    70e3dd8 View commit details
    Browse the repository at this point in the history

Commits on Aug 3, 2022

  1. Add square_roots_of_one_int

    @stuart-presnell
    stuart-presnell committed Aug 3, 2022
    Configuration menu
    Copy the full SHA
    dfc31fe View commit details
    Browse the repository at this point in the history

  2. Prove square_roots_of_one'' for zmod (p^α)

    @stuart-presnell
    stuart-presnell committed Aug 3, 2022
    Configuration menu
    Copy the full SHA
    b570938 View commit details
    Browse the repository at this point in the history

  3. Patch strong_probable_prime_of_prime_power_iff

    @stuart-presnell
    stuart-presnell committed Aug 3, 2022
    Configuration menu
    Copy the full SHA
    133c114 View commit details
    Browse the repository at this point in the history

  4. Insert proof of ord_compl_dvd_ord_compl_of_dvd

    @stuart-presnell
    stuart-presnell committed Aug 3, 2022
    Configuration menu
    Copy the full SHA
    25de5ec View commit details
    Browse the repository at this point in the history

  5. Add assumption hp_odd to spp...power_iff

    @stuart-presnell
    stuart-presnell committed Aug 3, 2022
    Configuration menu
    Copy the full SHA
    420f127 View commit details
    Browse the repository at this point in the history

  6. Confirm spp...power_iff has no sorrys

    @stuart-presnell
    stuart-presnell committed Aug 3, 2022
    Configuration menu
    Copy the full SHA
    8b0cdc5 View commit details
    Browse the repository at this point in the history

  7. docstring for first draft of Conrad Theorem 3.4

    @stuart-presnell
    stuart-presnell committed Aug 3, 2022
    Configuration menu
    Copy the full SHA
    55f80da View commit details
    Browse the repository at this point in the history

  8. Golf & rename square_roots_of_one_zmod

    @stuart-presnell
    stuart-presnell committed Aug 3, 2022
    Configuration menu
    Copy the full SHA
    9b3d7c4 View commit details
    Browse the repository at this point in the history

  9. Format and deal with some simps

    @stuart-presnell
    stuart-presnell committed Aug 3, 2022
    Configuration menu
    Copy the full SHA
    e8f82d7 View commit details
    Browse the repository at this point in the history

  10. Format braces

    @stuart-presnell
    stuart-presnell committed Aug 3, 2022
    Configuration menu
    Copy the full SHA
    a3375f1 View commit details
    Browse the repository at this point in the history

  11. Fix error at end of Theorem 3.4

    @stuart-presnell
    stuart-presnell committed Aug 3, 2022
    Configuration menu
    Copy the full SHA
    598b535 View commit details
    Browse the repository at this point in the history

  12. Tidy up pow_eq_one_subgroup

    @stuart-presnell
    stuart-presnell committed Aug 3, 2022
    Configuration menu
    Copy the full SHA
    98f2974 View commit details
    Browse the repository at this point in the history

  13. Tidy up pow_alt_subgroup

    @stuart-presnell
    stuart-presnell committed Aug 3, 2022
    Configuration menu
    Copy the full SHA
    adb9f2b View commit details
    Browse the repository at this point in the history

Commits on Aug 4, 2022

  1. Golf coprime_factorization_or_prime_power

    @stuart-presnell
    stuart-presnell committed Aug 4, 2022
    Configuration menu
    Copy the full SHA
    fce4a16 View commit details
    Browse the repository at this point in the history

  2. Golf one_or_coprime_factorization_or_prime_power

    @stuart-presnell
    stuart-presnell committed Aug 4, 2022
    Configuration menu
    Copy the full SHA
    df79f88 View commit details
    Browse the repository at this point in the history

  3. Golf card_closed_subset_dvd_card

    @stuart-presnell
    stuart-presnell committed Aug 4, 2022
    Configuration menu
    Copy the full SHA
    3c82d6a View commit details
    Browse the repository at this point in the history

  4. Golf card_le_half_of_proper_subgroup

    @stuart-presnell
    stuart-presnell committed Aug 4, 2022
    Configuration menu
    Copy the full SHA
    8bc050e View commit details
    Browse the repository at this point in the history

  5. Golf decidable_pred is_unit

    @stuart-presnell
    stuart-presnell committed Aug 4, 2022
    Configuration menu
    Copy the full SHA
    31485e2 View commit details
    Browse the repository at this point in the history

Commits on Aug 11, 2022

  1. Add import of is_prime_pow; rename coprime_add_one

    @stuart-presnell
    stuart-presnell committed Aug 11, 2022
    Configuration menu
    Copy the full SHA
    49b9472 View commit details
    Browse the repository at this point in the history

  2. Edit square_roots_of_one_zmod

    @stuart-presnell
    stuart-presnell committed Aug 11, 2022
    Configuration menu
    Copy the full SHA
    1013549 View commit details
    Browse the repository at this point in the history

  3. Add instance decidable_witness

    @stuart-presnell
    stuart-presnell committed Aug 11, 2022
    Configuration menu
    Copy the full SHA
    61a37d4 View commit details
    Browse the repository at this point in the history

  4. Add mul_pow_pred for ℕ and zmod n

    @stuart-presnell
    stuart-presnell committed Aug 11, 2022
    Configuration menu
    Copy the full SHA
    72a8e07 View commit details
    Browse the repository at this point in the history

  5. Add divider at end of Theorem 3.4

    @stuart-presnell
    stuart-presnell committed Aug 11, 2022
    Configuration menu
    Copy the full SHA
    0469ec7 View commit details
    Browse the repository at this point in the history

  6. Move up lemmas on subgroup cardinality

    @stuart-presnell
    stuart-presnell committed Aug 11, 2022
    Configuration menu
    Copy the full SHA
    e157954 View commit details
    Browse the repository at this point in the history

  7. Edit Thm 3.4 to use nat.miller_rabin_witness

    @stuart-presnell
    stuart-presnell committed Aug 11, 2022
    Configuration menu
    Copy the full SHA
    f76ab4b View commit details
    Browse the repository at this point in the history

  8. Fix typo

    @stuart-presnell
    stuart-presnell committed Aug 11, 2022
    Configuration menu
    Copy the full SHA
    e2527c0 View commit details
    Browse the repository at this point in the history

  9. Rename to MR_nonwitness_iff_miller_rabin_sequence

    @stuart-presnell
    stuart-presnell committed Aug 11, 2022
    Configuration menu
    Copy the full SHA
    38af6ba View commit details
    Browse the repository at this point in the history

Commits on Aug 12, 2022

  1. Move up lemmas about Fermat witnesses

    @stuart-presnell
    stuart-presnell committed Aug 12, 2022
    Configuration menu
    Copy the full SHA
    d3a29ee View commit details
    Browse the repository at this point in the history

  2. Prove fermat_nonwitness_mul

    @stuart-presnell
    stuart-presnell committed Aug 12, 2022
    Configuration menu
    Copy the full SHA
    c6e27e3 View commit details
    Browse the repository at this point in the history

  3. Prove fermat_nonwitness_of_prime

    @stuart-presnell
    stuart-presnell committed Aug 12, 2022
    Configuration menu
    Copy the full SHA
    7f6ab27 View commit details
    Browse the repository at this point in the history

  4. Prove MR_witness_iff_miller_rabin_sequence

    @stuart-presnell
    stuart-presnell committed Aug 12, 2022
    Configuration menu
    Copy the full SHA
    0d1b390 View commit details
    Browse the repository at this point in the history

Commits on Aug 13, 2022

  1. Some more computations

    @stuart-presnell
    stuart-presnell committed Aug 13, 2022
    Configuration menu
    Copy the full SHA
    ab22ffa View commit details
    Browse the repository at this point in the history

  2. Add pow_mul_eq_pow_pow_comm

    @stuart-presnell
    stuart-presnell committed Aug 13, 2022
    Configuration menu
    Copy the full SHA
    fb1e428 View commit details
    Browse the repository at this point in the history

Commits on Aug 15, 2022

  1. Add even_not_dvd_odd

    @stuart-presnell
    stuart-presnell committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    8411e2c View commit details
    Browse the repository at this point in the history

  2. Add eq_{neg_}one_of_eq_{neg_}one_modulus_dvd

    @stuart-presnell
    stuart-presnell committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    508e423 View commit details
    Browse the repository at this point in the history

  3. Add pow_mul_eq_pow_pow_comm

    @stuart-presnell
    stuart-presnell committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    94f2635 View commit details
    Browse the repository at this point in the history

Commits on Aug 29, 2022

  1. Merge branch 'master' into miller-rabin

    @stuart-presnell
    stuart-presnell committed Aug 29, 2022
    Configuration menu
    Copy the full SHA
    26c8ee0 View commit details
    Browse the repository at this point in the history

  2. Fix after renaming ord_{proj,compl}_mul

    @stuart-presnell
    stuart-presnell committed Aug 29, 2022
    Configuration menu
    Copy the full SHA
    0ac6272 View commit details
    Browse the repository at this point in the history

  3. Comment out sorried lemmas

    @stuart-presnell
    stuart-presnell committed Aug 29, 2022
    Configuration menu
    Copy the full SHA
    c9424ed View commit details
    Browse the repository at this point in the history

  4. Fix lint error

    @stuart-presnell
    stuart-presnell committed Aug 29, 2022
    Configuration menu
    Copy the full SHA
    42c9db8 View commit details
    Browse the repository at this point in the history

  5. Remove unused args

    @stuart-presnell
    stuart-presnell committed Aug 29, 2022
    Configuration menu
    Copy the full SHA
    54169ed View commit details
    Browse the repository at this point in the history