mathlib3
9a24b3e5 - chore(ring_theory/noetherian): rename `submodule.fg_map` to `submodule.fg.map` (#10688)

Commit
4 years ago
chore(ring_theory/noetherian): rename `submodule.fg_map` to `submodule.fg.map` (#10688) This renames: * `submodule.fg_map` to `submodule.fg.map` (to match `submonoid.fg.map` and enable dot notation) * `submodule.map_fg_of_fg` to `ideal.fg.map` * `submodule.fg_ker_ring_hom_comp` to `ideal.fg_ker_comp` to match `submodule.fg_ker_comp` and defines a new `ideal.fg` alias to avoid unfolding to `submodule R R` and `submodule.span`.
Author
Parents
Loading