feat(algebra/module/submodule/lattice): `submodule.is_maximal`

[haruhisa-enomoto]

This PR replaces the previous typeclass for maximal left ideals ideal.is_maximal : ideal R -> Prop with submodule.is_maximal : submodule R M -> Prop, which is a typeclass for maximal submodules of M. Some theorems are moved from namespace ideal to submodule so that for h : I.is_maximal for I : ideal R we can use dot notation h.is_prime.

Zulip

---

[urkud]

Could you please merge master? Otherwise LGTM. @eric-wieser, do you want to have another look? BTW, why most lemmas take (h : is_maximal _), not [is_maximal _]?

[bors[bot]]

:v: haruhisa-enomoto can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[Vierkantor]

BTW, why most lemmas take (h : is_maximal _), not [is_maximal _]?

I believe this is only a class to allow R / I to have a field instance when is_maximal I. In other cases, because ideals have nontrivial equalities, working with classes is inconvenient.