SUMO   View all facts   Glossary   Help

Entity > Abstract > Class > Relation > Function > BinaryFunction > AssociativeFunction > MultiplicationFn

MultiplicationFn
subject			fact

MultiplicationFn	documentation If ?NUMBER1 and ?NUMBER2 are Numbers, then (MultiplicationFn ?NUMBER1 ?NUMBER2) is the arithmetical product of these numbers
	has axiom (<=> (equal (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER) (equal (AdditionFn (MultiplicationFn (FloorFn (DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1))
	has axiom (=> (equal (SquareRootFn ?NUMBER1) ?NUMBER2) (equal (MultiplicationFn ?NUMBER2 ?NUMBER2) ?NUMBER1))
	has axiom (equal (MeasureFn ?NUMBER GigaHertz) (MeasureFn (MultiplicationFn ?NUMBER 1.0E9) Hertz))
	has axiom (equal 1 (MultiplicationFn ?NUMBER (ReciprocalFn ?NUMBER)))
	has axiom (equal (MeasureFn ?NUMBER Amu) (MeasureFn (MultiplicationFn ?NUMBER 1.6605402E-27) Kilogram))
	has axiom (equal (MeasureFn ?NUMBER Angstrom) (MeasureFn (MultiplicationFn ?NUMBER 1.0E-10) Meter))
	has axiom (equal (MeasureFn ?NUMBER BritishThermalUnit) (MeasureFn (MultiplicationFn ?NUMBER 1055.05585262) Joule))
	has axiom (equal (MeasureFn ?NUMBER Byte) (MeasureFn (MultiplicationFn ?NUMBER 8) Bit))
	has axiom (equal (MeasureFn ?NUMBER Calorie) (MeasureFn (MultiplicationFn ?NUMBER 4.1868) Joule))
	has axiom (equal (MeasureFn ?NUMBER Centimeter) (MeasureFn (MultiplicationFn ?NUMBER 0.01) Meter))
	has axiom (equal (MeasureFn ?NUMBER CentUnitedStates) (MeasureFn (MultiplicationFn ?NUMBER .01) DollarUnitedStates))
	has axiom (equal (MeasureFn ?NUMBER ElectronVolt) (MeasureFn (MultiplicationFn ?NUMBER 1.60217733E-19) Joule))
	has axiom (equal (MeasureFn ?NUMBER Foot) (MeasureFn (MultiplicationFn ?NUMBER 0.3048) Meter))
	has axiom (equal (MeasureFn ?NUMBER Inch) (MeasureFn (MultiplicationFn ?NUMBER 0.0254) Meter))
	has axiom (equal (MeasureFn ?NUMBER KiloByte) (MeasureFn (MultiplicationFn ?NUMBER 1024) Byte))
	has axiom (equal (MeasureFn ?NUMBER MegaByte) (MeasureFn (MultiplicationFn ?NUMBER 1024) KiloByte))
	has axiom (equal (MeasureFn ?NUMBER MegaHertz) (MeasureFn (MultiplicationFn ?NUMBER 1.0E6) Hertz))
	has axiom (equal (MeasureFn ?NUMBER Mile) (MeasureFn (MultiplicationFn ?NUMBER 1609.344) Meter))
	has axiom (equal (MeasureFn ?NUMBER MinuteDuration) (MeasureFn (MultiplicationFn ?NUMBER 60) SecondDuration))
	has axiom (equal (MeasureFn ?NUMBER Pound) (MeasureFn (MultiplicationFn ?NUMBER 0.45359237) Kilogram))
	has axiom (equal (MeasureFn ?NUMBER PoundForce) (MeasureFn (MultiplicationFn ?NUMBER 4.448222) Newton))
	has axiom (equal (MeasureFn ?NUMBER Rankine) (MeasureFn (MultiplicationFn ?NUMBER 1.8) Kelvin))
	has axiom (equal (MeasureFn ?NUMBER Slug) (MeasureFn (MultiplicationFn ?NUMBER 14.59390) Kilogram))
	has axiom (equal (MeasureFn ?NUMBER UnitedKingdomGallon) (MeasureFn (MultiplicationFn ?NUMBER 4.54609) Liter))
	has axiom (equal (MeasureFn ?NUMBER UnitedStatesGallon) (MeasureFn (MultiplicationFn ?NUMBER 3.785411784) Liter))
	has axiom (equal (MeasureFn ?NUMBER AngularDegree) (MeasureFn (MultiplicationFn ?NUMBER (DivisionFn Pi 180)) Radian))
	has axiom (equal (MeasureFn ?NUMBER DayDuration) (MeasureFn (MultiplicationFn ?NUMBER 24) HourDuration))
	has axiom (equal (MeasureFn ?NUMBER Gram) (MeasureFn (MultiplicationFn ?NUMBER 0.001) Kilogram))
	has axiom (equal (MeasureFn ?NUMBER HourDuration) (MeasureFn (MultiplicationFn ?NUMBER 60) MinuteDuration))
	has axiom (equal (MeasureFn ?NUMBER Kilogram) (MeasureFn (MultiplicationFn ?NUMBER 1000) Gram))
	has axiom (equal (MeasureFn ?NUMBER KiloHertz) (MeasureFn (MultiplicationFn ?NUMBER 1000) Hertz))
	has axiom (equal (MeasureFn ?NUMBER Kilometer) (MeasureFn (MultiplicationFn ?NUMBER 1000) Meter))
	has axiom (equal (MeasureFn ?NUMBER KiloWatt) (MeasureFn (MultiplicationFn ?NUMBER 1000) Watt))
	has axiom (equal (MeasureFn ?NUMBER MegaOhm) (MeasureFn (MultiplicationFn ?NUMBER 1.0E6) Ohm))
	has axiom (equal (MeasureFn ?NUMBER MegaPascal) (MeasureFn (MultiplicationFn ?NUMBER 1.0E6) Pascal))
	has axiom (equal (MeasureFn ?NUMBER MicroOhm) (MeasureFn (MultiplicationFn ?NUMBER 0.000001) Ohm))
	has axiom (equal (MeasureFn ?NUMBER MicroVolt) (MeasureFn (MultiplicationFn ?NUMBER 0.000001) Volt))
	has axiom (equal (MeasureFn ?NUMBER MilliAmpere) (MeasureFn (MultiplicationFn ?NUMBER .001) Ampere))
	has axiom (equal (MeasureFn ?NUMBER MilliVolt) (MeasureFn (MultiplicationFn ?NUMBER .001) Volt))
	has axiom (equal (MeasureFn ?NUMBER NanoAmpere) (MeasureFn (MultiplicationFn ?NUMBER 1.0E-9) Ampere))
	has axiom (equal (MeasureFn ?NUMBER NanoSecond) (MeasureFn (MultiplicationFn ?NUMBER 1.0E-9) Second))
	has axiom (equal (MeasureFn ?NUMBER PicoAmpere) (MeasureFn (MultiplicationFn ?NUMBER 1.0E-12) Ampere))
	has axiom (equal (MeasureFn ?NUMBER PicoSecond) (MeasureFn (MultiplicationFn ?NUMBER 1.0E-12) SecondDuration))
	has axiom (equal (MeasureFn ?NUMBER YearDuration) (MeasureFn (MultiplicationFn ?NUMBER 365) DayDuration))
	has domain1 Quantity
	has domain2 Quantity
	has identityElement 1
	has range Quantity
	is an instance of AssociativeFunction
	is an instance of CommutativeFunction
	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

Next AssociativeFunction: SubtractionFn    Up: AssociativeFunction, CommutativeFunction, RelationExtendedToQuantities    Previous AssociativeFunction: MinFn