Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-24 15:20 46ceb36e

View on Github →

refactor(*): rename semimodule to module, delete typeclasses module and vector_space (#7322) Splitting typeclasses between semimodule, module and vector_space was causing many (small) issues, so why don't we just get rid of this duplication? This PR contains the following changes:

  • delete the old module and vector_space synonyms for semimodule
  • find and replace all instances of semimodule and vector_space to module
  • (thereby renaming the previous semimodule typeclass to module)
  • rename vector_space.dim to module.rank (in preparation for generalizing this definition to all modules)
  • delete a couple module instances that have now become redundant This find-and-replace has been done extremely naïvely, but it seems there were almost no name clashes and no "clbuttic mistakes". I have gone through the full set of changes, finding nothing weird, and I'm fixing any build issues as they come up (I expect less than 10 declarations will cause conflicts). Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/module.20from.20semimodule.20over.20a.20ring A good example of a workaround required by the module abbreviation is the triv_sq_zero_ext.module instance.

Estimated changes

modified theorem dim_V
deleted theorem findim_V
added theorem finrank_V
modified theorem add_smul
modified theorem gsmul_eq_smul
modified theorem int.smul_one_eq_coe
added def module.comp_hom
added structure module.core
added def module.of_core
added theorem module.subsingleton
deleted def module
added theorem module_ext
modified theorem nat_smul_eq_nsmul
deleted def semimodule.comp_hom
deleted structure semimodule.core
deleted def semimodule.of_core
deleted theorem semimodule.subsingleton
deleted theorem semimodule_ext
deleted def vector_space
modified theorem linear_equiv.comp_coe
modified def linear_equiv.refl
modified theorem linear_equiv.refl_apply
modified theorem linear_equiv.symm_bijective
modified theorem linear_equiv.symm_trans
modified theorem linear_equiv.trans_symm
modified def linear_map.inverse
added theorem ordered_module.mk''
added theorem ordered_module.mk'
deleted theorem ordered_semimodule.mk''
deleted theorem ordered_semimodule.mk'
modified theorem smul_lt_smul_of_pos
modified theorem zero_smul_set
modified theorem concave_on.concave_le
modified theorem concave_on.smul
modified theorem convex_on.convex_le
modified theorem convex_on.smul
modified theorem neg_concave_on_iff
modified theorem neg_convex_on_iff
modified theorem caratheodory.shrink'
modified theorem caratheodory.step
modified structure enorm
modified def to_euclidean
deleted theorem findim_euclidean_space
modified theorem complex.dim_real_complex
modified theorem complex.{u}
deleted theorem findim_real_of_complex
modified theorem dfinsupp.support_smul
modified def equiv.linear_equiv
modified theorem finsupp.coe_smul
modified theorem finsupp.filter_smul
modified theorem finsupp.map_domain_smul
modified theorem finsupp.map_range_smul
modified theorem finsupp.smul_apply
modified theorem finsupp.smul_single
modified theorem finsupp.sum_smul_index'
modified theorem finsupp.support_smul
modified theorem matrix.block_diagonal'_smul
modified theorem matrix.block_diagonal_smul
modified theorem matrix.minor_smul
modified theorem mv_polynomial.coeff_smul
modified theorem polynomial.lhom_ext'
modified theorem polynomial.smul_monomial
modified theorem function.support_smul
modified theorem mv_polynomial.dim_R
deleted theorem mv_polynomial.findim_R
deleted theorem findim_alg_hom
added theorem finrank_alg_hom
modified theorem fixed_points.dim_le_card
modified def stereographic'
modified theorem stereographic'_source
modified theorem stereographic'_target
modified theorem times_cont_mdiff_coe_sphere
modified theorem times_cont_mdiff_neg_sphere
modified def collinear
modified theorem collinear_iff_dim_le_one
modified theorem midpoint_unique
modified theorem bilin_form.comp_comp
modified theorem bilin_form.comp_congr
modified theorem bilin_form.congr_comp
modified structure bilin_form
modified def dfinsupp.lsum
modified theorem dim_bot
modified theorem dim_eq_of_injective
modified theorem dim_eq_of_surjective
modified theorem dim_fin_fun
modified theorem dim_fun'
modified theorem dim_fun
modified theorem dim_le_of_submodule
modified theorem dim_le_of_surjective
modified theorem dim_le_one_iff
modified theorem dim_map_le
modified theorem dim_of_field
modified theorem dim_pi
modified theorem dim_pos
modified theorem dim_pos_iff_exists_ne_zero
modified theorem dim_pos_iff_nontrivial
modified theorem dim_prod
modified theorem dim_range_add_dim_ker
modified theorem dim_range_le
modified theorem dim_range_of_surjective
modified theorem dim_span_le
modified theorem dim_submodule_le
modified theorem dim_submodule_le_one_iff'
modified theorem dim_submodule_le_one_iff
modified theorem dim_top
modified theorem dim_zero_iff
modified theorem dim_zero_iff_forall_zero
modified theorem exists_is_basis_fintype
modified def rank
modified theorem rank_le_domain
modified theorem rank_le_range
deleted def vector_space.dim
added theorem module.dual_dim_eq
added theorem module.erange_coe
added theorem module.eval_ker
deleted theorem subspace.dual_findim_eq
deleted theorem vector_space.dual_dim_eq
deleted theorem vector_space.erange_coe
deleted theorem vector_space.eval_ker
modified theorem bot_eq_top_of_dim_eq_zero
modified theorem dim_eq_zero
deleted theorem findim_bot
deleted theorem findim_eq_zero
deleted theorem findim_span_eq_card
deleted theorem findim_span_le_card
deleted theorem findim_span_set_eq_card
deleted theorem findim_span_singleton
deleted theorem findim_top
added theorem finrank_bot
added theorem finrank_eq_zero
added theorem finrank_span_eq_card
added theorem finrank_span_le_card
added theorem finrank_span_singleton
added theorem finrank_top
deleted theorem is_basis_of_findim_zero'
deleted theorem is_basis_of_findim_zero
deleted theorem linear_equiv.findim_eq
modified theorem subalgebra.dim_bot
modified theorem subalgebra.dim_eq_one_iff
modified theorem subalgebra.dim_top
deleted theorem subalgebra.findim_bot
added theorem subalgebra.finrank_bot
deleted theorem submodule.findim_le
deleted theorem submodule.findim_lt
deleted theorem submodule.findim_mono
added theorem submodule.finrank_le
added theorem submodule.finrank_lt
added theorem submodule.finrank_mono
modified def equiv_of_dim_eq_dim
modified theorem finsupp.dim_eq
deleted theorem matrix.findim_matrix
added theorem matrix.finrank_matrix
modified theorem linear_map.apply_single
modified def linear_map.lsum
deleted theorem power_basis.findim
added theorem power_basis.finrank
modified theorem algebra.trace_algebra_map
modified theorem continuous_map.smul_apply
modified theorem continuous_map.smul_coe