## Division

This page discusses proper division where the result can be a fraction. Whole number division where the result is rounded down to the nearest whole number is described here.

### Definition

Division is defined by multiplying a number with its numerator and denominator reversed.

### Theorems

• (= (* A (/ B A)) B) /edit/peano_new/arithmetic/common/division.gh/divcani
• (= (/ A (1)) A) /edit/peano_new/arithmetic/common/division.gh/divid
• (= (* A (/ B C)) (/ (* A B) C)) /edit/peano_new/arithmetic/common/division.gh/divmulassi
• (= (* (/ A B) (/ C D)) (/ (* A C) (* B D))) /edit/peano_new/arithmetic/common/division.gh/fracmuli
• (= (/ (* A C) (* B C)) (/ A B)) /edit/peano_new/arithmetic/common/division.gh/fracFactorsi
• (= (+ (/ A C) (/ B C)) (/ (+ A B) C)) /edit/peano_new/arithmetic/common/division.gh/divdistri
• (= (+ (/ A B) (/ C D)) (/ (+ (* A D) (* B C)) (* B D))) /edit/peano_new/arithmetic/common/division.gh/addfraci
• (= (/ (/ A B) (/ C D)) (/ (* A D) (* B C))) /edit/peano_new/arithmetic/common/division.gh/divideFraci