Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(data/rat/basic): Add nat num and denom inv lemmas #8581

Closed
wants to merge 4 commits into from
Closed

[Merged by Bors] - feat(data/rat/basic): Add nat num and denom inv lemmas #8581

wants to merge 4 commits into from

Commits on Aug 8, 2021

  1. feat(rat.basic): Add nat num and denom inv lemmas

    @FrickHazard
    FrickHazard committed Aug 8, 2021
    Configuration menu
    Copy the full SHA
    b5a3e79 View commit details
    Browse the repository at this point in the history

Commits on Aug 9, 2021

  1. Update lemmas names to inv_coe_nat_num and inv_coe_nat_denom

    @FrickHazard
    FrickHazard committed Aug 9, 2021
    Configuration menu
    Copy the full SHA
    6a2c2c9 View commit details
    Browse the repository at this point in the history

Commits on Aug 11, 2021

  1. Add inv_coe_int_denom and inv_coe_int_num and golf nat proofs.

    @FrickHazard
    FrickHazard committed Aug 11, 2021
    Configuration menu
    Copy the full SHA
    97a7fe6 View commit details
    Browse the repository at this point in the history

  2. whitespace

    @eric-wieser
    eric-wieser committed Aug 11, 2021
    Configuration menu
    Copy the full SHA
    eefcac9 View commit details
    Browse the repository at this point in the history