Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-22 16:29 3e77fec2

View on Github →

feat(linear_algebra/finite_dimensional): finite dimensional vector spaces (#1241)

feat(linear_algebra/finite_dimensional): finite dimensional vector spaces
rw of_span_finite_eq_top to of_fg
prove infinite.nat_embedding
generalize finite_of_linear_independent to noetherian modules
fix build
fix build (ring_theory/polynomial)

Estimated changes

Modified src/data/fintype.lean

Modified src/linear_algebra/basis.lean

modified theorem eq_of_linear_independent_of_span_subtype

added theorem le_of_span_le_span

added theorem span_le_span_iff

Modified src/linear_algebra/dimension.lean

modified theorem dim_bot

added theorem dim_top

Created src/linear_algebra/finite_dimensional.lean

added theorem finite_dimensional.card_eq_findim

added theorem finite_dimensional.dim_lt_omega

added theorem finite_dimensional.eq_top_of_findim_eq

added theorem finite_dimensional.exists_is_basis_finite

added theorem finite_dimensional.findim_eq_dim

added theorem finite_dimensional.finite_dimensional_iff_dim_lt_omega

added theorem finite_dimensional.of_fg

added def finite_dimensional

added theorem linear_map.injective_iff_surjective

added theorem linear_map.ker_eq_bot_iff_range_eq_top

added theorem linear_map.mul_eq_one_comm

added theorem linear_map.mul_eq_one_of_mul_eq_one

added theorem linear_map.surjective_of_injective

Modified src/ring_theory/noetherian.lean

added theorem finite_of_linear_independent

modified theorem well_founded_submodule_gt

Modified src/ring_theory/polynomial.lean