FieldTheory.finite_primaryComponent_finiteExtension_of_fg
Over any finitely generated field, the primary roots of unity in every finite extension form a finite group, in arbitrary characteristic.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FieldTheory
universe u vLean source · statement
theorem finite_primaryComponent_finiteExtension_of_fg
(K : Type u) [Field K] (hfg : Field.FG K)
(L : Type v) [Field L] [Algebra K L] [FiniteDimensional K L]
(p : ℕ) [Fact p.Prime] : Finite (CommGroup.primaryComponent Lˣ p)