proposition: Lemma ideal_sum_zero_r I : I + ideal_zero R ↔ I.
proof: Proof. apply ideal_subset_antisymm. 1: apply ideal_sum_smallest. 1: reflexivity. 1: apply ideal_zero_subset. apply ideal_sum_subset_l. Defined.
imports: Basics Types Spaces.Finite.Fin Classes.interfaces.abstract_algebra Algebra.Rings.CRing Algebra.AbGroups