Prime

📁 Source: Mathlib/RingTheory/Prime.lean

Statistics

Metric	Count
Definitions	0
Theorems abs, neg, mul_eq_mul_prime_pow, mul_eq_mul_prime_prod	4
Total	4

Prime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs 📖	mathematical	Prime CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring	abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	—	abs_choice neg
neg 📖	mathematical	Prime CommSemiring.toCommMonoidWithZero CommRing.toCommSemiring	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing	—	neg_ne_zero IsUnit.neg_iff

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mul_eq_mul_prime_pow 📖	—	Prime MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero Monoid.toNatPow MonoidWithZero.toMonoid	—	—	mul_eq_mul_prime_prod Finset.prod_const Finset.card_range Finset.card_union_of_disjoint
mul_eq_mul_prime_prod 📖	mathematical	Prime MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero Finset.prod CommMonoidWithZero.toCommMonoid	Finset Finset.instUnion Disjoint Finset.partialOrder Finset.instOrderBot	—	Finset.induction Finset.union_idempotent mul_one Finset.mem_insert_self Finset.mem_insert_of_mem mul_assoc Finset.prod_insert Finset.mem_union_left Finset.mem_union_right Prime.dvd_or_dvd mul_comm Finset.insert_union Finset.disjoint_insert_left mul_right_inj' IsCancelMulZero.toIsLeftCancelMulZero Prime.ne_zero mul_left_comm Finset.union_insert Finset.disjoint_insert_right mul_left_inj' IsCancelMulZero.toIsRightCancelMulZero mul_right_comm

---

← Back to Index