Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-12 03:49 4ec7cc58

View on Github →

refactor(*): fix field names in linear_map and submodule (#3032)

  • linear_map now uses map_add' and map_smul';
  • submodule now extends add_submonoid and adds smul_mem';
  • no more submodule.is_add_subgroup instance;
  • open_subgroup now uses bundled subgroups;
  • is_linear_map is not a class anymore: we had a couple of instances but zero lemmas taking it as a typeclass argument;
  • subgroup.mem_coe now takes {g : G} as it should, not [g : G].

Estimated changes

modified def lie_algebra.Ad
deleted theorem is_linear_map.map_add
deleted theorem is_linear_map.map_smul
modified def is_linear_map.mk'
added structure is_linear_map
modified theorem linear_map.is_linear
modified theorem linear_map.map_add
modified theorem linear_map.map_smul
modified theorem submodule.add_mem
added theorem submodule.coe_set_eq
added theorem submodule.coe_sort_coe
modified theorem submodule.ext'
added theorem submodule.ext'_iff
modified theorem submodule.ext
modified theorem submodule.neg_mem_iff
modified theorem submodule.smul_mem
modified theorem submodule.sum_mem
modified theorem submodule.zero_mem
modified theorem subgroup.mem_coe
modified theorem linear_equiv.map_add
modified theorem linear_equiv.map_smul
modified theorem span_int_eq
added structure open_add_subgroup
modified theorem open_subgroup.ext'
modified theorem open_subgroup.ext
added theorem open_subgroup.ext_iff
deleted theorem open_subgroup.le_iff
added theorem open_subgroup.mem_coe
added structure open_subgroup
deleted def open_subgroup
added theorem subgroup.is_open_mono
added theorem submodule.is_open_mono