leftideal_generated@{u v} {R : Ring@{u}} (X : R -> Type@{v}) : LeftIdeal@{u v} R. Proof. snrapply Build_LeftIdeal. - snrapply Build_Subgroup'. + exact (fun x => merely (leftideal_generated_type X x)). + exact _. + apply tr, ligt_zero. + intros x y p q; strip_truncations. by apply tr, ligt_add_neg. - intros r x; apply Trunc_functor. apply ligt_mul. 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.