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 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 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 def collinear
modified theorem collinear_iff_dim_le_one
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
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