theorem
L22 ↗powerClass_eq_iff
ClassFieldTheory.powerClass_eq_iff
Two elements represent the same power class exactly when their ratio is an n-th power.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTheory
universe uLean source · statement
theorem powerClass_eq_iff
(K : Type u) [Field K] (n : ℕ+) (a b : Kˣ) :
powerClass K n a = powerClass K n b ↔
a / b ∈ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range