Divisors

📁 Source: Mathlib/Data/Nat/Factorization/Divisors.lean

Statistics

Metric	Count
Definitions	0
Theorems Iic_factorization_prod_pow_injective, Iio_factorization_prod_pow_injective, coe_divisors_eq_prod_pow_le_factorization, coe_properDivisors_eq_prod_pow_lt_factorization, divisors_eq_image_Iic_factorization_prod_pow, divisors_eq_map_attach_Iic_factorization_prod_pow, properDivisors_eq_image_Iio_factorization_prod_pow, properDivisors_eq_map_attach_Iio_factorization_prod_pow	8
Total	8

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Iic_factorization_prod_pow_injective 📖	mathematical	—	Finsupp MulZeroClass.toZero instMulZeroClass Finset SetLike.instMembership Finset.instSetLike Finset.Iic Finsupp.preorder instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Finsupp.orderBot instAddCommMonoid instPartialOrder instCanonicallyOrderedAdd Finsupp.instLocallyFiniteOrder instLocallyFiniteOrder factorization Finsupp.prod instCommMonoid Monoid.toPow instMonoid	—	—
Iio_factorization_prod_pow_injective 📖	mathematical	—	Finsupp MulZeroClass.toZero instMulZeroClass Finset SetLike.instMembership Finset.instSetLike Finset.Iio Finsupp.preorder instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Finsupp.orderBot instAddCommMonoid instPartialOrder instCanonicallyOrderedAdd Finsupp.instLocallyFiniteOrder instLocallyFiniteOrder factorization Finsupp.prod instCommMonoid Monoid.toPow instMonoid	—	—
coe_divisors_eq_prod_pow_le_factorization 📖	mathematical	—	SetLike.coe Finset Finset.instSetLike divisors setOf Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instLE factorization Finsupp.prod instCommMonoid Monoid.toPow instMonoid	—	Set.ext dvd_of_mem_divisors ne_zero_of_dvd_ne_zero factorization_le_iff_dvd prod_factorization_pow_eq_self mem_divisors Finsupp.prod_dvd_prod_of_subset_of_dvd Finsupp.support_mono instCanonicallyOrderedAdd
coe_properDivisors_eq_prod_pow_lt_factorization 📖	mathematical	—	SetLike.coe Finset Finset.instSetLike properDivisors setOf Finsupp MulZeroClass.toZero instMulZeroClass Preorder.toLT Finsupp.preorder instPreorder factorization Finsupp.prod instCommMonoid Monoid.toPow instMonoid	—	properDivisors_zero Finset.coe_empty factorization_zero Finsupp.instCanonicallyOrderedAddOfAddLeftMono instCanonicallyOrderedAdd instOrderedSub IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid Set.ext mem_properDivisors ne_zero_of_dvd_ne_zero lt_of_le_of_ne factorization_le_iff_dvd eq_of_factorization_eq' LT.lt.ne prod_factorization_pow_eq_self Finsupp.prod_dvd_prod_of_subset_of_dvd Finsupp.support_mono LT.lt.le factorization_prod_pow_eq_self_of_le_factorization
divisors_eq_image_Iic_factorization_prod_pow 📖	mathematical	—	divisors Finset.image Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.prod instCommMonoid Monoid.toPow instMonoid Finset.Iic Finsupp.preorder instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Finsupp.orderBot instAddCommMonoid instPartialOrder instCanonicallyOrderedAdd Finsupp.instLocallyFiniteOrder instLocallyFiniteOrder factorization	—	instCanonicallyOrderedAdd
divisors_eq_map_attach_Iic_factorization_prod_pow 📖	mathematical	—	divisors Finset.map Finsupp MulZeroClass.toZero instMulZeroClass Finset SetLike.instMembership Finset.instSetLike Finset.Iic Finsupp.preorder instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Finsupp.orderBot instAddCommMonoid instPartialOrder instCanonicallyOrderedAdd Finsupp.instLocallyFiniteOrder instLocallyFiniteOrder factorization Finsupp.prod instCommMonoid Monoid.toPow instMonoid Iic_factorization_prod_pow_injective Finset.attach	—	instCanonicallyOrderedAdd Iic_factorization_prod_pow_injective Finset.map_eq_image Finset.image_image Finset.attach_image_val divisors_eq_image_Iic_factorization_prod_pow
properDivisors_eq_image_Iio_factorization_prod_pow 📖	mathematical	—	properDivisors Finset.image Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.prod instCommMonoid Monoid.toPow instMonoid Finset.Iio Finsupp.preorder instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Finsupp.orderBot instAddCommMonoid instPartialOrder instCanonicallyOrderedAdd Finsupp.instLocallyFiniteOrder instLocallyFiniteOrder factorization	—	instCanonicallyOrderedAdd
properDivisors_eq_map_attach_Iio_factorization_prod_pow 📖	mathematical	—	properDivisors Finset.map Finsupp MulZeroClass.toZero instMulZeroClass Finset SetLike.instMembership Finset.instSetLike Finset.Iio Finsupp.preorder instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Finsupp.orderBot instAddCommMonoid instPartialOrder instCanonicallyOrderedAdd Finsupp.instLocallyFiniteOrder instLocallyFiniteOrder factorization Finsupp.prod instCommMonoid Monoid.toPow instMonoid Iio_factorization_prod_pow_injective Finset.attach	—	instCanonicallyOrderedAdd Iio_factorization_prod_pow_injective Finset.map_eq_image Finset.image_image Finset.attach_image_val properDivisors_eq_image_Iio_factorization_prod_pow

---

← Back to Index