proposition: Lemma ideal_intresection_unit_l I : ideal_unit R ∩ I ↔ I.
proof: Proof. apply ideal_subset_antisymm. 1: apply ideal_intersection_subset_r. apply ideal_intersection_subset. 1: apply ideal_unit_subset. reflexivity. Defined.
imports: Basics Types Spaces.Finite.Fin Classes.interfaces.abstract_algebra Algebra.Rings.CRing Algebra.AbGroups