*DivisionFn* | *documentation* If ?NUMBER1 *and* ?NUMBER2 are Numbers, then (*DivisionFn* ?NUMBER1 ?NUMBER2) is the result of dividing ?NUMBER1 by ?NUMBER2. An exception occurs when ?NUMBER1 = 1, in which case (*DivisionFn* ?NUMBER1 ?NUMBER2) is the reciprocal of ?NUMBER2 | |

**has axiom** (*<=>* (*equal* (*RemainderFn* ?NUMBER1 ?NUMBER2) ?NUMBER) (*equal* (*AdditionFn* (*MultiplicationFn* (*FloorFn* (*DivisionFn* ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1))
| |

**has axiom** (=> (*instance* ?NUMBER RationalNumber) (exists (?INT1 ?INT2) (*and* (*instance* ?INT1 Integer) (*instance* ?INT2 Integer) (*equal* ?NUMBER (*DivisionFn* ?INT1 ?INT2)))))
| |

**has axiom** (*equal* (*TangentFn* ?DEGREE) (*DivisionFn* (*SineFn* ?DEGREE) (*CosineFn* ?DEGREE)))
| |

**has axiom** (*equal* (*MeasureFn* ?NUMBER *Cup*) (*MeasureFn* (*DivisionFn* ?NUMBER 2) *Pint*))
| |

**has axiom** (*equal* (*MeasureFn* ?NUMBER *Ounce*) (*MeasureFn* (*DivisionFn* ?NUMBER 8) *Cup*))
| |

**has axiom** (*equal* (*MeasureFn* ?NUMBER *Pint*) (*MeasureFn* (*DivisionFn* ?NUMBER 2) *Quart*))
| |

**has axiom** (*equal* (*MeasureFn* ?NUMBER *Quart*) (*MeasureFn* (*DivisionFn* ?NUMBER 4) *UnitedStatesGallon*))
| |

**has axiom** (*equal* (*MeasureFn* ?NUMBER *AngularDegree*) (*MeasureFn* (*MultiplicationFn* ?NUMBER (*DivisionFn* Pi 180)) *Radian*))
| |

**has domain1** Quantity | |

**has domain2** Quantity | |

**has ***identityElement* 1 | |

**has ***range* Quantity | |

**is an ***instance* of AssociativeFunction | |

**is an ***instance* of RelationExtendedToQuantities | |

BinaryFunction | **is first ***domain* of *distributes* | |

**is first ***domain* of *identityElement* | |

**is second ***domain* of *distributes* | |

Relation | **is first ***domain* of *domain* | |

**is first ***domain* of *domainSubclass* | |

**is first ***domain* of *holds* | |

**is first ***domain* of *subrelation* | |

**is first ***domain* of *valence* | |

**is second ***domain* of *subrelation* | |

Class | **is third ***domain* of *domain* | |

**is third ***domain* of *domainSubclass* | |

Abstract | **is ***disjoint* from Physical | |