Prime

📁 Source: Mathlib/Data/PNat/Prime.lean

Statistics

Metric	Count
Definitions `coePNat`, `toPNat`, `Prime`, `gcd`, `lcm`	5
Theorems `coe_pnat_inj`, `coe_pnat_injective`, `coe_pnat_nat`, `coprime_dvd_left`, `factor_eq_gcd_left`, `factor_eq_gcd_left_right`, `factor_eq_gcd_right`, `factor_eq_gcd_right_right`, `gcd_mul`, `gcd_mul_left_cancel`, `gcd_mul_left_cancel_right`, `gcd_mul_right_cancel`, `gcd_mul_right_cancel_right`, `mul`, `mul_right`, `pow`, `ne_one`, `not_dvd_one`, `one_lt`, `coprime_coe`, `coprime_one`, `dvd_gcd`, `dvd_lcm_left`, `dvd_lcm_right`, `dvd_prime`, `eq_one_of_lt_two`, `exists_prime_and_dvd`, `fact_prime_five`, `fact_prime_three`, `fact_prime_two`, `gcd_coe`, `gcd_comm`, `gcd_dvd_left`, `gcd_dvd_right`, `gcd_eq_left`, `gcd_eq_left_iff_dvd`, `gcd_eq_right_iff_dvd`, `gcd_mul_lcm`, `gcd_one`, `instFactPrimeValOfPrime`, `lcm_coe`, `lcm_dvd`, `not_prime_one`, `one_coprime`, `one_gcd`, `prime_five`, `prime_three`, `prime_two`	48
Total	53

Nat.Primes

Definitions

Name	Category	Theorems
`coePNat` 📖	CompOp	—
`toPNat` 📖	CompOp	7 math math: `coe_pnat_injective`, `coe_pnat_nat`, `PNat.count_factorMultiset`, `PrimeMultiset.prod_ofPrime`, `PNat.factorMultiset_ofPrime`, `PrimeMultiset.coePNat_ofPrime`, `coe_pnat_inj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_pnat_inj` 📖	mathematical	—	`toPNat`	—	`coe_pnat_injective`
`coe_pnat_injective` 📖	mathematical	—	`Nat.Primes` `PNat` `toPNat`	—	—
`coe_pnat_nat` 📖	mathematical	—	`PNat.val` `toPNat` `Nat.Prime`	—	—

PNat

Definitions

Name	Category	Theorems
`Prime` 📖	MathDef	10 math math: `not_prime_one`, `fact_prime_two`, `prime_five`, `exists_prime_and_dvd`, `prime_two`, `fact_prime_five`, `fact_prime_three`, `mem_factorMultiset`, `PrimeMultiset.coePNat_prime`, `prime_three`
`gcd` 📖	CompOp	27 math math: `gcd_rel_left`, `gcd_b_eq`, `gcd_rel_right`, `gcd_coe`, `Coprime.factor_eq_gcd_right_right`, `Coprime.gcd_mul_right_cancel`, `gcd_dvd_right`, `gcd_eq_right_iff_dvd`, `factorMultiset_gcd`, `Coprime.gcd_mul_right_cancel_right`, `Coprime.gcd_mul_left_cancel`, `one_gcd`, `dvd_gcd`, `Coprime.factor_eq_gcd_right`, `PrimeMultiset.prod_inf`, `gcd_mul_lcm`, `Coprime.gcd_mul`, `gcd_dvd_left`, `gcd_comm`, `gcd_one`, `Coprime.factor_eq_gcd_left`, `gcd_eq`, `Coprime.factor_eq_gcd_left_right`, `Coprime.gcd_mul_left_cancel_right`, `gcd_eq_left`, `gcd_a_eq`, `gcd_eq_left_iff_dvd`
`lcm` 📖	CompOp	7 math math: `lcm_dvd`, `lcm_coe`, `dvd_lcm_right`, `PrimeMultiset.prod_sup`, `gcd_mul_lcm`, `dvd_lcm_left`, `factorMultiset_lcm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coprime_coe` 📖	mathematical	—	`val` `Coprime`	—	—
`coprime_one` 📖	mathematical	—	`Coprime` `PNat` `instOfNatPNatOfNeZeroNat`	—	`Coprime.symm` `one_coprime`
`dvd_gcd` 📖	mathematical	`PNat` `semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `instCommMonoid`	`gcd`	—	`dvd_iff`
`dvd_lcm_left` 📖	mathematical	—	`PNat` `semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `instCommMonoid` `lcm`	—	`dvd_iff`
`dvd_lcm_right` 📖	mathematical	—	`PNat` `semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `instCommMonoid` `lcm`	—	`dvd_iff`
`dvd_prime` 📖	mathematical	`Prime`	`PNat` `semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `instCommMonoid` `instOfNatPNatOfNeZeroNat`	—	`dvd_iff` `Nat.dvd_prime`
`eq_one_of_lt_two` 📖	—	`PNat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat` `instOfNatPNatOfNeZeroNat`	—	—	`le_antisymm` `lt_add_one_iff` `one_le`
`exists_prime_and_dvd` 📖	mathematical	—	`Prime` `PNat` `semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `instCommMonoid`	—	`Nat.exists_prime_and_dvd` `coe_eq_one_iff` `Nat.Prime.pos` `dvd_iff`
`fact_prime_five` 📖	mathematical	—	`Fact` `Prime` `PNat` `instOfNatPNatOfNeZeroNat`	—	`prime_five`
`fact_prime_three` 📖	mathematical	—	`Fact` `Prime` `PNat` `instOfNatPNatOfNeZeroNat`	—	`prime_three`
`fact_prime_two` 📖	mathematical	—	`Fact` `Prime` `PNat` `instOfNatPNatOfNeZeroNat`	—	`prime_two`
`gcd_coe` 📖	mathematical	—	`val` `gcd`	—	—
`gcd_comm` 📖	mathematical	—	`gcd`	—	`eq`
`gcd_dvd_left` 📖	mathematical	—	`PNat` `semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `instCommMonoid` `gcd`	—	`dvd_iff`
`gcd_dvd_right` 📖	mathematical	—	`PNat` `semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `instCommMonoid` `gcd`	—	`dvd_iff`
`gcd_eq_left` 📖	mathematical	`PNat` `semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `instCommMonoid`	`gcd`	—	`gcd_eq_left_iff_dvd`
`gcd_eq_left_iff_dvd` 📖	mathematical	—	`gcd` `PNat` `semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `instCommMonoid`	—	`dvd_iff`
`gcd_eq_right_iff_dvd` 📖	mathematical	—	`gcd` `PNat` `semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `instCommMonoid`	—	`gcd_comm` `gcd_eq_left_iff_dvd`
`gcd_mul_lcm` 📖	mathematical	—	`PNat` `instMulPNat` `gcd` `lcm`	—	—
`gcd_one` 📖	mathematical	—	`gcd` `PNat` `instOfNatPNatOfNeZeroNat`	—	`gcd_comm` `one_gcd`
`instFactPrimeValOfPrime` 📖	mathematical	—	`Fact` `Nat.Prime` `val`	—	—
`lcm_coe` 📖	mathematical	—	`val` `lcm`	—	—
`lcm_dvd` 📖	mathematical	`PNat` `semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `instCommMonoid`	`lcm`	—	`dvd_iff`
`not_prime_one` 📖	mathematical	—	`Prime` `PNat` `instOfNatPNatOfNeZeroNat`	—	`Nat.not_prime_one`
`one_coprime` 📖	mathematical	—	`Coprime` `PNat` `instOfNatPNatOfNeZeroNat`	—	`one_gcd`
`one_gcd` 📖	mathematical	—	`gcd` `PNat` `instOfNatPNatOfNeZeroNat`	—	`gcd_eq_left_iff_dvd` `one_dvd`
`prime_five` 📖	mathematical	—	`Prime` `PNat` `instOfNatPNatOfNeZeroNat`	—	`Nat.prime_five`
`prime_three` 📖	mathematical	—	`Prime` `PNat` `instOfNatPNatOfNeZeroNat`	—	`Nat.prime_three`
`prime_two` 📖	mathematical	—	`Prime` `PNat` `instOfNatPNatOfNeZeroNat`	—	`Nat.prime_two`

PNat.Coprime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coprime_dvd_left` 📖	—	`PNat` `semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `PNat.instCommMonoid` `PNat.Coprime`	—	—	`PNat.dvd_iff` `PNat.coprime_coe`
`factor_eq_gcd_left` 📖	mathematical	`PNat.Coprime` `PNat` `semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `PNat.instCommMonoid`	`PNat.gcd` `instMulPNat`	—	`PNat.gcd_eq_left_iff_dvd` `gcd_mul_right_cancel` `coprime_dvd_left` `symm`
`factor_eq_gcd_left_right` 📖	mathematical	`PNat.Coprime` `PNat` `semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `PNat.instCommMonoid`	`PNat.gcd` `instMulPNat`	—	`PNat.gcd_comm` `factor_eq_gcd_left`
`factor_eq_gcd_right` 📖	mathematical	`PNat.Coprime` `PNat` `semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `PNat.instCommMonoid`	`PNat.gcd` `instMulPNat`	—	`mul_comm` `factor_eq_gcd_left`
`factor_eq_gcd_right_right` 📖	mathematical	`PNat.Coprime` `PNat` `semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `PNat.instCommMonoid`	`PNat.gcd` `instMulPNat`	—	`PNat.gcd_comm` `factor_eq_gcd_right`
`gcd_mul` 📖	mathematical	`PNat.Coprime`	`PNat.gcd` `PNat` `instMulPNat`	—	`PNat.eq` `PNat.coprime_coe`
`gcd_mul_left_cancel` 📖	mathematical	`PNat.Coprime`	`PNat.gcd` `PNat` `instMulPNat`	—	`PNat.eq`
`gcd_mul_left_cancel_right` 📖	mathematical	`PNat.Coprime`	`PNat.gcd` `PNat` `instMulPNat`	—	`PNat.gcd_comm` `gcd_mul_left_cancel`
`gcd_mul_right_cancel` 📖	mathematical	`PNat.Coprime`	`PNat.gcd` `PNat` `instMulPNat`	—	`mul_comm` `gcd_mul_left_cancel`
`gcd_mul_right_cancel_right` 📖	mathematical	`PNat.Coprime`	`PNat.gcd` `PNat` `instMulPNat`	—	`mul_comm` `gcd_mul_left_cancel_right`
`mul` 📖	mathematical	`PNat.Coprime`	`PNat` `instMulPNat`	—	`PNat.coprime_coe` `PNat.mul_coe`
`mul_right` 📖	mathematical	`PNat.Coprime`	`PNat` `instMulPNat`	—	`PNat.coprime_coe` `PNat.mul_coe`
`pow` 📖	mathematical	`PNat.Coprime`	`Monoid.toNatPow` `Nat.instMonoid` `PNat.val`	—	`PNat.coprime_coe`

PNat.Prime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ne_one` 📖	—	`PNat.Prime`	—	—	`Nat.Prime.ne_one` `PNat.coe_eq_one_iff`
`not_dvd_one` 📖	mathematical	`PNat.Prime`	`PNat` `semigroupDvd` `Monoid.toSemigroup` `CommMonoid.toMonoid` `PNat.instCommMonoid` `instOfNatPNatOfNeZeroNat`	—	`PNat.dvd_iff` `Nat.Prime.not_dvd_one`
`one_lt` 📖	mathematical	`PNat.Prime`	`PNat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat` `instOfNatPNatOfNeZeroNat`	—	`Nat.Prime.one_lt`

---

← Back to Index