(I : Ideal R) : Ann I ↔ ideal_zero R :: I. Proof. intros x; split. - intros [p q]; strip_truncations; split; apply tr; intros y i. + exact (p y i). + exact (q y i). - intros [p q]; strip_truncations; split; apply tr; intros y i. + exact (p y i). + exact (q y i). 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.