Library HoTT.Algebra.Rings

Basic theory

Require Export HoTT.Algebra.Rings.Ring.
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.