mathlib
mathlib copied to clipboard
leanprover-community
feat(algebra/module/submodule/lattice): `submodule.is_maximal`
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.
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 _]?
: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.
![bors[bot] avatar](https://avatars.githubusercontent.com/in/1847?v=4 "Published by a pub.dev verified publisher"){kind=small}
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.
