Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-13 05:19 51f7319b

View on Github →

chore(algebra/module): rename type vars, minor cleanup, add module docstring (#2392)

  • Use R, S for rings, k for a field, M, M₂ etc for modules;
  • Add a semiring version of ring_hom.to_module;
  • Stop using {rα : ring α} trick as Lean 3.7 tries unification before class search;
  • Add a short module docstring

Estimated changes

modified theorem finset.sum_const'
modified theorem finset.sum_smul
modified def ideal
modified theorem is_linear_map.map_neg
modified theorem is_linear_map.map_smul
modified theorem is_linear_map.map_sub
modified theorem is_linear_map.map_zero
modified def is_linear_map.mk'
modified theorem is_linear_map.mk'_apply
modified theorem linear_map.coe_mk
modified def linear_map.comp
modified theorem linear_map.comp_apply
modified theorem linear_map.ext
modified theorem linear_map.ext_iff
modified def linear_map.id
modified theorem linear_map.id_apply
modified theorem linear_map.is_linear
modified theorem linear_map.map_add
modified theorem linear_map.map_neg
modified theorem linear_map.map_smul
modified theorem linear_map.map_sub
modified theorem linear_map.map_sum
modified theorem linear_map.to_fun_eq_coe
modified structure linear_map
modified theorem list.sum_smul
modified structure module.core
modified theorem module.gsmul_eq_smul
modified def module.of_core
modified theorem multiset.sum_smul
modified theorem neg_one_smul
modified def ring_hom.to_module
modified theorem smul_eq_mul
modified theorem smul_sub
modified theorem sub_smul
modified theorem submodule.coe_add
modified theorem submodule.coe_mk
modified theorem submodule.coe_neg
modified theorem submodule.coe_smul
modified theorem submodule.coe_sub
modified theorem submodule.coe_zero
modified theorem submodule.ext'
modified theorem submodule.ext
modified theorem submodule.mem_coe
modified theorem submodule.neg_mem
modified theorem submodule.smul_mem
modified theorem submodule.smul_mem_iff'
modified theorem submodule.subtype_eq_val
modified theorem submodule.sum_mem
modified theorem submodule.zero_mem
modified structure submodule
modified def subspace
modified def vector_space
modified theorem zero_smul