proposition: Lemma ideal_quotient_intersection (I J K : Ideal R) : (I ∩ J :: K) ↔ (I :: K) ∩ (J :: K).
proof: Proof. apply ideal_subset_antisymm. 1: intros r p; hnf in p; split; hnf; intros; by apply p. intros r [p q]; hnf in p, q; intros x k; by split; [apply p | apply q]. Defined.
imports: Basics Types Spaces.Finite.Fin Classes.interfaces.abstract_algebra Algebra.Rings.CRing Algebra.AbGroups