mathlib

4ec7cc58 - refactor(*): fix field names in `linear_map` and `submodule` (#3032)

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]`.