HOL html
| Files Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Theorems Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
X (theorems)
XY_ARE_SOLUTIONSXY_COPRIME
XY_EXP
XY_EXP_LEMMA
XY_GCD
XY_GCD_LEMMA
XY_POWER_NEG
XY_POWER_POS
XY_Y3_CONGRUENCE
X_CLAUSES
X_CONGRUENT
X_CONGRUENT_2NJ_NEG
X_CONGRUENT_2NJ_NEG_LEMMA
X_CONGRUENT_2NJ_POS
X_CONGRUENT_4MNJ_POS
X_CONGRUENT_4NJ_POS
X_DEGENERATE
X_INCREASES
X_INCREASES_LE
X_INCREASES_LT
X_INCREASES_SUC
X_INJ
x_diff_y2
xi_DEF
xmaxQ_exists
xmaxQ_max
xmaxQexists_lemma
xminQ_exists
xminQ_min
xminQexists_lemma
xmin_le_xmax
xmin_lt_xmax