norm_num
extensions for Ordinals #
The default norm_num
extensions for many operators requires a semiring,
which without a right distributive law, ordinals do not have.
We must therefore define new extensions for them.
The norm_num
extension for multiplication on ordinals.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The norm_num
extension for inequality on ordinals.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The norm_num
extension for strict inequality on ordinals.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The norm_num
extension for subtration on ordinals.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The norm_num
extension for division on ordinals.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The norm_num
extension for modulo on ordinals.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The norm_num
extension for homogenous power on ordinals.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The norm_num
extension for natural power on ordinals.
Equations
- One or more equations did not get rendered due to their size.