Ideal quotients

Ideal quotient versions of some basic results.

theorem Ideal.Quotient.mk_out' {R : Type u_1} [CommRing R] {I : Ideal R} (x : R ⧸ I) : (Ideal.Quotient.mk I) (Quotient.out' x) = x

theorem Ideal.Quotient.out_sub {R : Type u_1} [CommRing R] (I : Ideal R) (x : R) : Quotient.out' ((Ideal.Quotient.mk I) x) - x ∈ I

theorem Ideal.Quotient.out_sub_dvd {R : Type u_1} [CommRing R] {I : Ideal R} {y : R} (x : R) (hI : I = Ideal.span {y}) : y ∣ Quotient.out' ((Ideal.Quotient.mk I) x) - x