The n-th power classes of ℝ

For n ≠ 0, the quotient ℝˣ ⧸ (ℝˣ)ⁿ has as many elements as there are n-th roots of unity in ℝ: one for odd n, two for even n. This is the local count at a real place of a number field.

Main results

• TauCeti.card_powerClasses_real: #(ℝˣ ⧸ (ℝˣ)ⁿ) = #μ_n(ℝ) for n ≠ 0.

theorem TauCeti.card_powerClasses_real {n : ℕ} (hn : n ≠ 0) : Nat.card (ℝˣ ⧸ (powMonoidHom n).range) = Nat.card ↥(rootsOfUnity n ℝ)

The n-th power classes of ℝ. For n ≠ 0, the quotient ℝˣ ⧸ (ℝˣ)ⁿ has as many elements as there are n-th roots of unity in ℝ: one for odd n, two for even n.