Add
Add_with_order
- - other theorems
Core
DerivMul
Distances
- Properties of distances
- Limits
- Cauchy sequences and completeness
- Continuity
- Derivability
- Properties of distances and limits
Div
- For the Rocq tactic "ring"
- Commutative field
Div_with_order
Ideals
IterAdd
IterAnd
IterMax
IterMul
Lap_algebra
Misc
Mul
Mul_with_order
Nat_algebra
Order
PermutationFun
Polynomial_algebra
RealLike
Structures
Utils
- Iterators for aggregation operations
- List_cart_prod
- List_extract
- List_rank
- List_map2
- binomial
Z_algebra

This page has been generated by coqdoc