(** Basic theory *)Require Export HoTT.Algebra.Rings.CRing. Require Export HoTT.Algebra.Rings.Ideal. Require Export HoTT.Algebra.Rings.QuotientRing. Require Export HoTT.Algebra.Rings.ChineseRemainder. (** Examples *) Require Export HoTT.Algebra.Rings.Z.