(I J K : Ideal R) : (I ∩ J :: K) ↔ (I :: K) ∩ (J :: K). Proof. apply ideal_subset_antisymm. - intros r [p q]; strip_truncations; split; split; apply tr; intros x k. 1,3: by apply p. 1,2: by apply q. - intros r [[p q] [u v]]. strip_truncations; split; apply tr; intros x k; split. + by apply p. + by apply u. + by apply q. + by apply v. Defined.
Require Import Basics Types. Require Import Spaces.Finite.Fin. Require Import Classes.interfaces.canonical_names. Require Import Algebra.Rings.Ring. Require Import Algebra.Groups.Subgroup. Require Import Algebra.AbGroups. Require Import WildCat.Core. Module Import Notation.