[Merged by Bors] - feat(NumberTheory.NumberField.Basic): add mem_span_integralBasis#5996
[Merged by Bors] - feat(NumberTheory.NumberField.Basic): add mem_span_integralBasis#5996
Conversation
|
Why not having an actual |
This is what we are doing here. We start with a ℤ-basis of |
|
Ah, I see, |
I added the general result theorem Basis.localizationLocalization_span {ι : Type _} (b : Basis ι R A) :
Submodule.span R (Set.range (b.localizationLocalization Rₛ S Aₛ)) =
Submodule.map (IsScalarTower.toAlgHom R A Aₛ) ⊤ and used it to prove |
|
@Vierkantor can you have a look at this? Thanks! |
|
Sure! I will make some time in the coming days. |
|
Not sure why "Detect changes to header SHAs / Add annotations (pull_request) " is taking forever... |
It seems merging master solved this. |
Riccardo, thanks a lot for your improvements of this PR. I am in Japan at the moment and it is difficult to find time to work on Lean. I added your name as a co-author. Maybe I should also update the title and description? |
Vierkantor
left a comment
There was a problem hiding this comment.
This is indeed a useful result, thanks for spotting that we're missing it.
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
|
@Vierkantor Thanks for the review. As you suggested, I moved |
Add the following result:
```lean
theorem mem_span_integralBasis {x : K} :
x ∈ Submodule.span ℤ (Set.range (integralBasis K)) ↔ x ∈ 𝓞 K
```
that is, `integralBasis` is indeed a `ℤ`-basis of the ring of integers.
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
Add the following result:
```lean
theorem mem_span_integralBasis {x : K} :
x ∈ Submodule.span ℤ (Set.range (integralBasis K)) ↔ x ∈ 𝓞 K
```
that is, `integralBasis` is indeed a `ℤ`-basis of the ring of integers.
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
Add the following result:
```lean
theorem mem_span_integralBasis {x : K} :
x ∈ Submodule.span ℤ (Set.range (integralBasis K)) ↔ x ∈ 𝓞 K
```
that is, `integralBasis` is indeed a `ℤ`-basis of the ring of integers.
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
Add the following result:
```lean
theorem mem_span_integralBasis {x : K} :
x ∈ Submodule.span ℤ (Set.range (integralBasis K)) ↔ x ∈ 𝓞 K
```
that is, `integralBasis` is indeed a `ℤ`-basis of the ring of integers.
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
Add the following result:
that is,
integralBasisis indeed aℤ-basis of the ring of integers.Co-authored-by: Riccardo Brasca riccardo.brasca@gmail.com