NatDivisors

📁 Source: Mathlib/Data/Finset/NatDivisors.lean

Statistics

Metric	Count
Definitions divisorsHom	1
Theorems nat_divisors_prod, nat_divisors_prod, nat_divisors_prod, divisors_sq, divisorsHom_apply, divisors_mul	6
Total	7

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nat_divisors_prod 📖	mathematical	—	Nat.divisors prod Nat.instCommMonoid Finset commMonoid	—	map_prod MonoidHom.instMonoidHomClass

List

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nat_divisors_prod 📖	mathematical	—	Nat.divisors Nat.instOne Finset Finset.mul Finset.one	—	map_list_prod MonoidHom.instMonoidHomClass

Multiset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nat_divisors_prod 📖	mathematical	—	Nat.divisors prod Nat.instCommMonoid Finset Finset.commMonoid map	—	map_multiset_prod MonoidHom.instMonoidHomClass

Nat

Definitions

Name	Category	Theorems
divisorsHom 📖	CompOp	1 math math: divisorsHom_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
divisorsHom_apply 📖	mathematical	—	DFunLike.coe MonoidHom Finset MulOneClass.toMulOne instMulOneClass Finset.mulOneClass MonoidHom.instFunLike divisorsHom divisors	—	—
divisors_mul 📖	mathematical	—	divisors Finset Finset.mul	—	Finset.ext IsDomain.to_noZeroDivisors instIsDomain

Nat.Prime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
divisors_sq 📖	mathematical	Nat.Prime	Nat.divisors Monoid.toNatPow Nat.instMonoid Finset Finset.instInsert Finset.instSingleton	—	Nat.pow_right_injective two_le Nat.divisors_prime_pow Finset.range_add_one Finset.instLawfulSingleton Finset.map_insert pow_one Finset.map_singleton pow_zero

---

← Back to Index