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.

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

[Merged by Bors] - chore(ring_theory): split localization.lean and dedekind_domain.lean #12206

Closed
wants to merge 6 commits into from

Commits on Feb 21, 2022

  1. chore(ring_theory/localization): split into multiple files

    All the lines in `localization.lean` are nearly identically available in the other files:
    
    ```bash
    $ src/ring_theory/localization/*.lean | sort | comm -23 <(sort src/ring_theory/localization.lean) -
    Authors: Kenny Lau, Mario Carneiro, Johan Commelin, Amelia Livingston
    end
    is_domain_localization (le_non_zero_divisors_of_no_zero_divisors
    is_domain_of_le_non_zero_divisors K (le_refl (non_zero_divisors A))
     * `is_localization.is_integer` is a predicate stating that `x : S` is in the image of `R`
    open_locale big_operators
    section
    variables (A K) (C : Type*)
    variables (A) [unique_factorization_monoid A]
    variables (K : Type*)
    variables (M N)
    variables (M) {S}
    variables (R)
    variables (R) {A : Type*} [comm_ring A] [is_domain A]
    variables {R M} (S) {K : Type*}
    variables {Rₘ Sₘ}
    variables (S Q M)
    ```
    Vierkantor committed Feb 21, 2022
    Configuration menu
    Copy the full SHA
    1f04964 View commit details
    Browse the repository at this point in the history
  2. Update imports

    Vierkantor committed Feb 21, 2022
    Configuration menu
    Copy the full SHA
    2d7ec43 View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    e307f96 View commit details
    Browse the repository at this point in the history

Commits on Feb 22, 2022

  1. Optimize imports

    Vierkantor committed Feb 22, 2022
    Configuration menu
    Copy the full SHA
    fbdeb3d View commit details
    Browse the repository at this point in the history
  2. Fix imports

    Vierkantor committed Feb 22, 2022
    Configuration menu
    Copy the full SHA
    8299df5 View commit details
    Browse the repository at this point in the history
  3. More import fixing

    Vierkantor committed Feb 22, 2022
    Configuration menu
    Copy the full SHA
    8bb6918 View commit details
    Browse the repository at this point in the history