Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-10 15:18 6d2cbf9d

View on Github →

feat(ring_theory/artinian): Artinian modules (#9009)

Estimated changes

Created src/ring_theory/artinian.lean

added theorem is_artinian.bijective_of_injective_endomorphism

added theorem is_artinian.disjoint_partial_infs_eventually_top

added theorem is_artinian.exists_endomorphism_iterate_ker_sup_range_eq_top

added theorem is_artinian.finite_of_linear_independent

added theorem is_artinian.induction

added theorem is_artinian.surjective_of_injective_endomorphism

added theorem is_artinian_iff_well_founded

added theorem is_artinian_of_fg_of_artinian'

added theorem is_artinian_of_fg_of_artinian

added theorem is_artinian_of_fintype

added theorem is_artinian_of_injective

added theorem is_artinian_of_le

added theorem is_artinian_of_linear_equiv

added theorem is_artinian_of_quotient_of_artinian

added theorem is_artinian_of_range_eq_ker

added theorem is_artinian_of_submodule_of_artinian

added theorem is_artinian_of_surjective

added theorem is_artinian_of_tower

added theorem is_artinian_ring_iff

added theorem is_artinian_ring_of_ring_equiv

added theorem is_artinian_ring_of_surjective

added theorem is_artinian_span_of_finite

added theorem monotone_stabilizes_iff_artinian

added theorem ring.is_artinian_of_zero_eq_one

added theorem set_has_minimal_iff_artinrian