proposition: Lemma ideal_quotient_unit_bottom (I : Ideal R) : (I :: ideal_unit R) ↔ I.
proof: Proof. apply ideal_subset_antisymm. { intros r p. rewrite <- rng_mult_one_r. exact (p cring_one tt). } apply ideal_quotient_subset. Defined.
imports: Basics Types Spaces.Finite.Fin Classes.interfaces.abstract_algebra Algebra.Rings.CRing Algebra.AbGroups