English
A Noetherian K-module V is finitely generated and conversely; equivalence stated as IsNoetherian K V ↔ Module.Finite K V.
Русский
Noetherian K-модуль V порождается конечной связкой и наоборот; эквивалентность: IsNoetherian K V ⇔ Module.Finite K V.
LaTeX
$$$ IsNoetherian K V \\iff Module.Finite K V $$$
Lean4
/-- The subfield of F fixed by the field endomorphism `m`. -/
def subfield : Subfield F where
carrier := fixedBy F m
zero_mem' := smul_zero m
add_mem' hx hy := (smul_add m _ _).trans <| congr_arg₂ _ hx hy
neg_mem' hx := (smul_neg m _).trans <| congr_arg _ hx
one_mem' := smul_one m
mul_mem' hx hy := (smul_mul' m _ _).trans <| congr_arg₂ _ hx hy
inv_mem' x hx := (smul_inv'' m x).trans <| congr_arg _ hx
