proposition: Lemma ideal_intersection_subset (I J K : Ideal R) : K ⊆ I -> K ⊆ J -> K ⊆ I ∩ J.
proof: Proof. intros p q x r; specialize (p x r); specialize (q x r); by split. Defined.
imports: Basics Types Spaces.Finite.Fin Classes.interfaces.abstract_algebra Algebra.Rings.CRing Algebra.AbGroups