theorem
L15 ↗fg_of_finiteDimensional
FieldTheory.fg_of_finiteDimensional
Finite extensions of finitely generated fields are finitely generated.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FieldTheory
universe u vLean source · statement
theorem fg_of_finiteDimensional
(K : Type u) (L : Type v) [Field K] [Field L] [Algebra K L]
[FiniteDimensional K L] (hfg : Field.FG K) : Field.FG L