NumberField.Units.rootsOfUnity_eq_torsion
theorem NumberField.Units.rootsOfUnity_eq_torsion :
β (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
rootsOfUnity (NumberField.Units.torsionOrder K) β₯(NumberField.ringOfIntegers K) = NumberField.Units.torsion K
This theorem states that in a given number field `K`, the group of roots of unity of order dividing the order of the torsion subgroup of the group of units is equal to the torsion subgroup itself. In other words, the set of elements in the ring of integers of `K` whose power of the order of the torsion subgroup equals 1 is precisely the same set of elements that form the torsion subgroup in the group of units of the ring of integers.
More concisely: The group of roots of unity of order dividing the order of the torsion subgroup in the group of units of the ring of integers of a number field equals the torsion subgroup itself.
|
NumberField.Units.rootsOfUnity_eq_one
theorem NumberField.Units.rootsOfUnity_eq_one :
β (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {k : β+},
(βk).Coprime β(NumberField.Units.torsionOrder K) β
β {ΞΆ : (β₯(NumberField.ringOfIntegers K))Λ£}, ΞΆ β rootsOfUnity k β₯(NumberField.ringOfIntegers K) β ΞΆ = 1
This theorem states that for a any number field `K` and a positive integer `k` that is coprime with the order of the torsion subgroup of the field's unit group, all roots of unity in the ring of integers of the field with order dividing `k` are trivial, i.e., are equal to 1. In other words, if `k` does not divide the order of the torsion subgroup, then there are no nontrivial (different from 1) roots of unity in the ring of integers of the number field with an order that is a divisor of `k`.
More concisely: For a number field K and a positive integer k coprime to the order of its unit group's torsion subgroup, there are no nontrivial k-th roots of unity in the ring of integers of K.
|