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: the finite adele ring is an algebra over the finite integral adeles. #13705

Closed
wants to merge 6 commits into from
Closed

[Merged by Bors] - feat: the finite adele ring is an algebra over the finite integral adeles. #13705

wants to merge 6 commits into from

Commits on Jun 10, 2024

  1. feat: the finite adele ring is an algebra over the finite integral ad… 

    …eles.
    @kbuzzard
    kbuzzard committed Jun 10, 2024
    Configuration menu
    Copy the full SHA
    6a5c0f7 View commit details
    Browse the repository at this point in the history

Commits on Jun 14, 2024

  1. make FiniteAdeleRing a subtype not a subalgebra

    @kbuzzard
    kbuzzard committed Jun 14, 2024
    Configuration menu
    Copy the full SHA
    0c97ac6 View commit details
    Browse the repository at this point in the history

  2. move lemma to nearer the relevant definition

    @kbuzzard
    kbuzzard committed Jun 14, 2024
    Configuration menu
    Copy the full SHA
    b18dcb2 View commit details
    Browse the repository at this point in the history

  3. add docstring

    @kbuzzard
    kbuzzard committed Jun 14, 2024
    Configuration menu
    Copy the full SHA
    ef29552 View commit details
    Browse the repository at this point in the history

Commits on Jun 26, 2024

  1. Update Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean 

    Co-authored-by: Oliver Nash <[email protected]>
    @kbuzzard @ocfnash
    kbuzzard and ocfnash authored Jun 26, 2024
    Configuration menu
    Copy the full SHA
    7d4ea98 View commit details
    Browse the repository at this point in the history

  2. long lines (thanks Oliver ;-) )

    @kbuzzard
    kbuzzard committed Jun 26, 2024
    Configuration menu
    Copy the full SHA
    b23e33f View commit details
    Browse the repository at this point in the history