Annihilators of residue classes

For an ideal I of a commutative ring R and c : R, the annihilator of the class of c in R ⧸ I, written as the colon ideal (⊥ : Submodule R (R ⧸ I)).colon {Ideal.Quotient.mk I c}, is the ideal quotient (I : c) = {r | r * c ∈ I}. This is the form in which associated primes of R ⧸ I appear (isAssociatedPrime_iff).

Main results

• TauCeti.Ideal.Quotient.mem_colon_singleton_mk: r annihilates the class of c in R ⧸ I exactly when r * c ∈ I.

theorem TauCeti.Ideal.Quotient.mem_colon_singleton_mk {R : Type u_1} [CommRing R] {I : Ideal R} {c r : R} : r ∈ ⊥.colon {(Ideal.Quotient.mk I) c} ↔ r * c ∈ I

An element r annihilates the class of c in R ⧸ I exactly when r * c ∈ I.