Prime

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

Statistics

Metric	Count
Definitions Prime, decidablePrime, minFac, decidablePrime, minFac, minFacAux	6
Theorems minFac_to_nat, minFacAux_to_nat, minFac_to_nat	3
Total	9

Num

Definitions

Name	Category	Theorems
Prime 📖	MathDef	—
decidablePrime 📖	CompOp	—
minFac 📖	CompOp	1 math math: minFac_to_nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
minFac_to_nat 📖	mathematical	—	castPosNum Nat.instOne minFac Nat.minFac castNum MulZeroClass.toZero Nat.instMulZeroClass	—	PosNum.minFac_to_nat

PosNum

Definitions

Name	Category	Theorems
decidablePrime 📖	CompOp	—
minFac 📖	CompOp	1 math math: minFac_to_nat
minFacAux 📖	CompOp	1 math math: minFacAux_to_nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
minFacAux_to_nat 📖	mathematical	castPosNum Nat.instOne bit1	minFacAux Nat.minFacAux	—	minFacAux.eq_1 Nat.minFacAux.eq_1 Nat.sqrt_lt minFacAux.eq_2 Nat.instIsStrictOrderedRing cast_succ add_left_comm add_assoc
minFac_to_nat 📖	mathematical	—	castPosNum Nat.instOne minFac Nat.minFac	—	Nat.minFac_one minFac.eq_3 Nat.minFac_eq Nat.instAtLeastTwoHAddOfNat minFacAux_to_nat Nat.sqrt_lt IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Nat.instIsStrictOrderedRing mul_add Distrib.leftDistribClass mul_one IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toMulPosStrictMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono Nat.instNontrivial covariant_swap_add_of_covariant_add IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add Nat.instCanonicallyOrderedAdd minFac.eq_2

---

← Back to Index