Ihs-math
The default theory of +, -, *, /, and EXPT for the IHS library.
This theory simply consists of the theories integerp-algebra
and expt-algebra.
This theory is the default theory exported by the ihs/math-lemmas book.
This theory will normally be ENABLEd by every book in the IHS library.
Subtopics
- Expt-algebra
- A theory of EXPT which is compatible with the ALGEBRA theories.
- Integerp-algebra
- A basic theory of algebra for all INTEGERPs.
