proposition: Lemma ideal_product_unit_l I : ideal_unit R ⋅ I ↔ I.
proof: Proof. apply ideal_subset_antisymm. 1: apply ideal_product_subset_r. intros r p. rewrite <- rng_mult_one_l. by apply tr, sgt_in, ipn_in. Defined.
imports: Basics Types Spaces.Finite.Fin Classes.interfaces.abstract_algebra Algebra.Rings.CRing Algebra.AbGroups