Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-17 15:21 ba24b38b

View on Github →

feat(ring_theory/noetherian): fg_pi (#10845)

Estimated changes

Modified src/linear_algebra/free_module/strong_rank_condition.lean

Modified src/linear_algebra/pi.lean

added theorem submodule.pi_empty

added theorem submodule.pi_mono

added theorem submodule.pi_top

Modified src/ring_theory/finiteness.lean

Modified src/ring_theory/noetherian.lean

added theorem submodule.fg_pi