Mathlib Changelog
Changelog
About
Github
Commit
2022-12-07 12:47
a652f6c3
View on Github →
feat(ring_theory/ideal/associated_prime): Define associated primes of a module. (
#17065
)
Estimated changes
Created
src/ring_theory/ideal/associated_prime.lean
added
theorem
associate_primes.mem_iff
added
theorem
associated_primes.eq_empty_of_subsingleton
added
theorem
associated_primes.eq_singleton_of_is_primary
added
theorem
associated_primes.nonempty
added
theorem
associated_primes.subset_of_injective
added
def
associated_primes
added
theorem
exists_le_is_associated_prime_of_is_noetherian_ring
added
theorem
is_associated_prime.annihilator_le
added
theorem
is_associated_prime.eq_radical
added
theorem
is_associated_prime.is_prime
added
theorem
is_associated_prime.map_of_injective
added
def
is_associated_prime
added
theorem
linear_equiv.associated_primes.eq
added
theorem
linear_equiv.is_associated_prime_iff
added
theorem
not_is_associated_prime_of_subsingleton