Mathlib v3 is deprecated. Go to Mathlib v4

Theorem subalgebra.fg_bot_to_submodule

Modification history

2022-11-18 14:15

src/ring_theory/finiteness.lean

chore(ring_theory): move `submodule.fg` to `ring_theory.finiteness` (#17541) …

Modified subalgebra.fg_bot_to_submodule View on Github →

2022-01-17 00:42

src/ring_theory/noetherian.lean

feat(*): add to_sub* lemmas for `map`, `fg` (#11480) …

Added subalgebra.fg_bot_to_submodule View on Github →