(I : Ideal R) : (I :: ideal_unit R) ↔ I. Proof. apply ideal_subset_antisymm. - intros r [p q]. strip_truncations. rewrite <- rng_mult_one_r. exact (p ring_one tt). - apply ideal_quotient_subset. 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.