(I J K : Ideal R) : (I + J) ⋅ K ↔ I ⋅ K + J ⋅ K. Proof. apply ideal_subset_antisymm. { intros r p. strip_truncations. induction p as [ r i | | r s p1 IHp1 p2 IHp2]. - destruct i as [r s p q]. strip_truncations. induction p as [ t k | | t k p1 IHp1 p2 IHp2 ]. + apply tr, sgt_in. destruct k as [j | k]. * left; by apply tr, sgt_in, ipn_in. * right; by apply tr, sgt_in, ipn_in. + apply tr, sgt_in; left. rewrite rng_mult_zero_l. apply ideal_in_zero. + rewrite rng_dist_r. rewrite rng_mult_negate_l. by apply ideal_in_plus_negate. - apply ideal_in_zero. - by apply ideal_in_plus_negate. } apply ideal_sum_smallest. 1,2: apply ideal_product_subset_pres_l. 1: apply ideal_sum_subset_l. apply ideal_sum_subset_r. 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.