Metamath Proof Explorer
Table of Contents - 6.2.2. Coprimality and Euclid's lemma (cont.)
This section is about coprimality with respect to primes, and a special
version of Euclid's lemma for primes is provided, see euclemma.
- coprm
- prmrp
- euclemma
- isprm6
- prmdvdsexp
- prmdvdsexpb
- prmdvdsexpr
- prmdvdssq
- prmexpb
- prmfac1
- dvdszzq
- rpexp
- rpexp1i
- rpexp12i
- prmndvdsfaclt
- prmdvdsbc
- prmdvdsncoprmbd
- ncoprmlnprm
- cncongrprm
- isevengcd2
- isoddgcd1
- 3lcm2e6