Add
Add_with_order
Order Compatibility
rngl_order_compatibility works for pair (≤, <)
rngl_order_compatibility works for pair (<, ≤)
generic theorems: work for pair (≤, <) and for pair (<, ≤)
specific theorems: version for ≤, followed with version for <
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
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