Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-20 02:00 1016a140

View on Github →

refactor(linear_algebra/finite_dimensional): generalize finite_dimensional.iff_fg to division rings (#7644) Replace finite_dimensional.iff_fg (working over a field) with is_noetherian.iff_fg (working over a division ring). Also, use the module.finite predicate.

Estimated changes

Modified src/analysis/normed_space/inner_product.lean

Modified src/data/complex/is_R_or_C.lean

Modified src/field_theory/finite/polynomial.lean

Created src/field_theory/finiteness.lean

added theorem is_noetherian.coe_finset_basis_index

added theorem is_noetherian.dim_lt_omega

added theorem is_noetherian.finite_basis_index

added theorem is_noetherian.iff_dim_lt_omega

added theorem is_noetherian.iff_fg

added theorem is_noetherian.range_finset_basis

Modified src/field_theory/fixed.lean

Modified src/field_theory/splitting_field.lean

Modified src/field_theory/tower.lean

Modified src/linear_algebra/dimension.lean

Modified src/linear_algebra/dual.lean

Modified src/linear_algebra/finite_dimensional.lean

deleted theorem finite_dimensional.coe_finset_basis_index

deleted theorem finite_dimensional.dim_lt_omega

deleted theorem finite_dimensional.finite_basis_index

deleted theorem finite_dimensional.finite_dimensional_iff_dim_lt_omega

deleted theorem finite_dimensional.iff_fg

deleted theorem finite_dimensional.range_finset_basis

Modified src/linear_algebra/finsupp_vector_space.lean

Modified src/ring_theory/finiteness.lean

modified theorem module.finite_def

Modified src/ring_theory/noetherian.lean

modified theorem finite_of_linear_independent