[Merged by Bors] - feat(NumberTheory.NumberField.Units): add torsion subgroup#5748
[Merged by Bors] - feat(NumberTheory.NumberField.Units): add torsion subgroup#5748
Conversation
|
Please remember to add the label |
riccardobrasca
left a comment
There was a problem hiding this comment.
We probably want also the fact that the double coercion from (𝓞 K)ˣ to 𝓞 K to K is the same as the coercion from (𝓞 K)ˣ to K.
LGTM but I am not very familiar with coercions in Lean4. You can maybe ask on Zulip.
As you suggested, I asked for some expert opinion on Zulip |
|
✌️ xroblot can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
We define the torsion subgroup of the units of a number field and prove some results about it, mostly: it is finite, cyclic and an unit is torsion iff its value is 1 at all infinite places. Some results linking to `rootsOfUnity` are also proved. This PR also includes a direct coercion from `(𝓞 K)ˣ` to `K` that is very convenient, although I am not sure it's done properly.
|
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. |
We define the torsion subgroup of the units of a number field and prove some results about it, mostly: it is finite, cyclic and an unit is torsion iff its value is 1 at all infinite places. Some results linking to `rootsOfUnity` are also proved. This PR also includes a direct coercion from `(𝓞 K)ˣ` to `K` that is very convenient, although I am not sure it's done properly.
We define the torsion subgroup of the units of a number field and prove some results about it, mostly: it is finite, cyclic and an unit is torsion iff its value is 1 at all infinite places. Some results linking to `rootsOfUnity` are also proved. This PR also includes a direct coercion from `(𝓞 K)ˣ` to `K` that is very convenient, although I am not sure it's done properly.
We define the torsion subgroup of the units of a number field and prove some results about it, mostly: it is finite, cyclic and an unit is torsion iff its value is 1 at all infinite places. Some results linking to `rootsOfUnity` are also proved. This PR also includes a direct coercion from `(𝓞 K)ˣ` to `K` that is very convenient, although I am not sure it's done properly.
We define the torsion subgroup of the units of a number field and prove some results about it, mostly: it is finite, cyclic and
an unit is torsion iff its value is 1 at all infinite places. Some results linking to
rootsOfUnityare also proved.This PR also includes a direct coercion from
(𝓞 K)ˣtoKthat is very convenient, although I am not sure it's done properly.