Theorem module.finite.of_injective
Modification history
2022-11-18 14:15
src/ring_theory/finiteness.lean
chore(ring_theory): move `submodule.fg` to `ring_theory.finiteness` (#17541) …
Modified module.finite.of_injectiveView on Github →2021-10-23 14:30
src/ring_theory/finiteness.lean
feat(ring_theory/noetherian): generalize to semiring (#9881) …
Modified module.finite.of_injectiveView on Github →