Commit 2023-04-10 19:09 487009f2

View on Github →

feat: port FieldTheory.Finiteness (#3373)

Estimated changes

Modified Mathlib.lean

Created Mathlib/FieldTheory/Finiteness.lean

added theorem IsNoetherian.coeSort_finsetBasisIndex

added theorem IsNoetherian.coe_finsetBasisIndex

added theorem IsNoetherian.finite_basis_index

added theorem IsNoetherian.iff_fg

added theorem IsNoetherian.iff_rank_lt_aleph0

added theorem IsNoetherian.range_finsetBasis

added theorem IsNoetherian.rank_lt_aleph0