{R S : Ring} (f : R $-> S) (I : Ideal S) : ideal_extension f (ideal_preimage f I) ⊆ I. Proof. intros x. apply Trunc_rec. intros y. induction y. + destruct x as [s [p q]]. destruct q; exact p. + apply ideal_in_zero. + by apply ideal_in_plus_negate. + by rapply isleftideal. + by rapply isrightideal. 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.