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