The n-th power classes of an algebraically closed field

For n ≠ 0, every unit of an algebraically closed field F is an n-th power, so the quotient Fˣ ⧸ (Fˣ)ⁿ is trivial. This is the local count at a complex place of a number field.

Main results

• TauCeti.card_powerClasses_of_isAlgClosed: #(Fˣ ⧸ (Fˣ)ⁿ) = 1 for n ≠ 0.

theorem TauCeti.card_powerClasses_of_isAlgClosed {F : Type u_1} [Field F] [IsAlgClosed F] {n : ℕ} (hn : n ≠ 0) : Nat.card (Fˣ ⧸ (powMonoidHom n).range) = 1

The n-th power classes of an algebraically closed field. For n ≠ 0, every unit of an algebraically closed field is an n-th power, so Fˣ ⧸ (Fˣ)ⁿ is trivial.