Rocq Ring-Like: A Library for Ring-Like Algebraic Structures

Welcome to the RingLike library documentation!

This library provides a flexible and modular framework to work with algebraic structures such as semirings, rings, and fields, as well as their generalizations on various types like integers, polynomials, matrices, and more.

Quick start

• To learn about the basic concepts and usage, see the Core module documentation.
• To explore examples and advanced features, browse the other generated HTML files.

About RingLike

RingLike represents algebraic structures with optional operations such as opposite (negation), subtraction, inverse, and division, enabling smooth handling of semirings, rings, and fields in a unified way.

Whether you work with natural numbers, integers, rationals, or more complex structures, RingLike provides a clean interface and solid foundation.

Available Modules

• Core

• Structures
• Order
• Add
• Mul
• Div
• Add_with_order
• Mul_with_order
• Div_with_order
• Distances

• IterAdd
• IterMul
• IterAnd
• IterMax

• RealLike
• IntermVal
• PermutationFun
• DerivMul
• Utils
• Misc

Algebras

• Nat_algebra
• Z_algebra
• Lap_algebra
• Polynomial_algebra

Table of Contents

• toc

This documentation is generated automatically. For the latest source code and updates, visit the GitHub repository.