(** Basic theory *)

Require Export HoTT.Algebra.Rings.Ring.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Export HoTT.Algebra.Rings.CRing.
Require Export HoTT.Algebra.Rings.Ideal.
Require Export HoTT.Algebra.Rings.Module.
Require Export HoTT.Algebra.Rings.QuotientRing.
Require Export HoTT.Algebra.Rings.Localization.
Require Export HoTT.Algebra.Rings.ChineseRemainder.
Require Export HoTT.Algebra.Rings.KroneckerDelta.
Require Export HoTT.Algebra.Rings.Idempotent.

(** Examples *)

Require Export HoTT.Algebra.Rings.Z.
Require Export HoTT.Algebra.Rings.Vector.
Require Export HoTT.Algebra.Rings.Matrix.