Squarefree

📁 Source: Mathlib/Data/Nat/Squarefree.lean

Statistics

Metric	Count
Definitions `MinSqFacProp`, `instDecidablePredSquarefree`, `minSqFac`, `minSqFacAux`, `Squarefree`	5
Theorems `ext_iff`, `coprime_div_gcd_of_squarefree`, `coprime_of_squarefree_mul`, `divisors_filter_squarefree`, `divisors_filter_squarefree_of_squarefree`, `factorization_eq_one_of_squarefree`, `minSqFacAux_has_prop`, `minSqFacProp_div`, `minSqFac_dvd`, `minSqFac_has_prop`, `minSqFac_le_of_dvd`, `minSqFac_prime`, `primeFactors_div_gcd`, `primeFactors_prod`, `prod_primeFactors_invOn_squarefree`, `prod_primeFactors_of_squarefree`, `prod_primeFactors_sdiff_of_squarefree`, `sq_mul_squarefree`, `sq_mul_squarefree_of_pos`, `sq_mul_squarefree_of_pos'`, `squarefree_and_prime_pow_iff_prime`, `squarefree_iff_factorization_le_one`, `squarefree_iff_minSqFac`, `squarefree_iff_nodup_primeFactorsList`, `squarefree_iff_prime_squarefree`, `squarefree_mul`, `squarefree_mul_iff`, `squarefree_of_factorization_le_one`, `squarefree_pow_iff`, `squarefree_two`, `sum_divisors_filter_squarefree`, `natFactorization_le_one`, `nodup_primeFactorsList`	33
Total	38

Nat

Definitions

Name	Category	Theorems
`MinSqFacProp` 📖	MathDef	2 math math: `minSqFacAux_has_prop`, `minSqFac_has_prop`
`instDecidablePredSquarefree` 📖	CompOp	5 math math: `divisors_filter_squarefree_of_squarefree`, `ArithmeticFunction.moebius_sq`, `sum_divisors_filter_squarefree`, `divisors_filter_squarefree`, `ArithmeticFunction.abs_moebius`
`minSqFac` 📖	CompOp	2 math math: `minSqFac_has_prop`, `squarefree_iff_minSqFac`
`minSqFacAux` 📖	CompOp	1 math math: `minSqFacAux_has_prop`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coprime_div_gcd_of_squarefree` 📖	—	`Squarefree` `instMonoid`	—	—	`coprime_of_squarefree_mul` `Ne.bot_lt`
`coprime_of_squarefree_mul` 📖	—	`Squarefree` `instMonoid`	—	—	`coprime_of_dvd` `squarefree_iff_prime_squarefree` `mul_dvd_mul`
`divisors_filter_squarefree` 📖	mathematical	—	`Finset.val` `Finset.filter` `Squarefree` `instMonoid` `instDecidablePredSquarefree` `divisors` `Multiset.map` `Finset` `Multiset.prod` `instCommMonoid` `Finset.powerset` `Multiset.toFinset` `UniqueFactorizationMonoid.normalizedFactors` `instCommMonoidWithZero` `NormalizationMonoid.ofUniqueUnits` `Unique.instSubsingleton` `Units` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `unique_units` `instUniqueFactorizationMonoid`	—	`Unique.instSubsingleton` `instUniqueFactorizationMonoid` `Multiset.Nodup.ext` `Finset.nodup` `Multiset.Nodup.map_on` `Multiset.rel_eq` `associated_eq_eq` `UniqueFactorizationMonoid.factors_unique` `UniqueFactorizationMonoid.irreducible_of_normalized_factor` `Multiset.mem_toFinset` `Finset.mem_powerset` `Finset.mem_def` `associated_iff_eq` `Multiset.toFinset_subset` `Multiset.toFinset_val` `Multiset.Nodup.dedup` `UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors` `mul_ne_zero_iff` `IsStrictOrderedRing.noZeroDivisors` `instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `instCanonicallyOrderedAdd` `UniqueFactorizationMonoid.normalizedFactors_mul` `Multiset.subset_of_le` `Multiset.le_add_right` `UniqueFactorizationMonoid.prod_normalizedFactors` `Multiset.prod_eq_zero_iff` `instNontrivial` `not_irreducible_zero` `Multiset.mem_dedup` `Multiset.mem_of_le` `Finset.val_le_iff` `Associated.dvd_iff_dvd_right` `Associated.symm` `Multiset.prod_dvd_prod_of_le` `le_trans` `Multiset.dedup_le`
`divisors_filter_squarefree_of_squarefree` 📖	mathematical	`Squarefree` `instMonoid`	`Finset.filter` `instDecidablePredSquarefree` `divisors`	—	`Finset.ext` `Finset.filter_subset` `Finset.mem_filter` `Squarefree.squarefree_of_dvd` `dvd_of_mem_divisors`
`factorization_eq_one_of_squarefree` 📖	mathematical	`Squarefree` `instMonoid` `Prime`	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `instMulZeroClass` `Finsupp.instFunLike` `factorization`	—	`LE.le.antisymm` `Squarefree.natFactorization_le_one` `Prime.dvd_iff_one_le_factorization` `Squarefree.ne_zero` `instNontrivial`
`minSqFacAux_has_prop` 📖	mathematical	—	`MinSqFacProp` `minSqFacAux`	—	—
`minSqFacProp_div` 📖	—	`Prime` `MinSqFacProp`	—	—	`coprime_primes` `MinSqFacProp.eq_1` `squarefree_iff_prime_squarefree` `dvd_trans` `dvd_mul_left`
`minSqFac_dvd` 📖	—	`minSqFac`	—	—	`minSqFac_has_prop`
`minSqFac_has_prop` 📖	mathematical	—	`MinSqFacProp` `minSqFac`	—	`prime_two` `Prime.two_le` `minSqFacProp_div` `minSqFacAux_has_prop` `lt_of_le_of_ne`
`minSqFac_le_of_dvd` 📖	—	`minSqFac`	—	—	`minSqFac_has_prop` `minFac_dvd` `le_trans` `minFac_prime` `dvd_trans` `mul_dvd_mul` `minFac_le` `lt_of_lt_of_le`
`minSqFac_prime` 📖	mathematical	`minSqFac`	`Prime`	—	`minSqFac_has_prop`
`primeFactors_div_gcd` 📖	mathematical	`Squarefree` `instMonoid`	`primeFactors` `Finset` `Finset.instSDiff`	—	`Finset.ext` `Ne.bot_lt` `Squarefree.ne_zero` `instNontrivial` `dvd_of_mul_left_dvd` `Irreducible.not_isUnit` `Dvd.dvd.trans` `mul_dvd_mul_right` `Prime.coprime_iff_not_dvd`
`primeFactors_prod` 📖	mathematical	`Prime`	`primeFactors` `Finset.prod` `instCommMonoid`	—	`Finset.prod_ne_zero_iff` `instNontrivial` `IsStrictOrderedRing.noZeroDivisors` `instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `instCanonicallyOrderedAdd` `Prime.ne_zero` `Finset.ext` `mem_primeFactors_of_ne_zero` `Prime.dvd_finset_prod_iff` `Prime.prime` `Prime.dvd_iff_eq` `Prime.ne_one` `dvd_rfl`
`prod_primeFactors_invOn_squarefree` 📖	mathematical	—	`Set.InvOn` `Finset` `Finsupp.support` `MulZeroClass.toZero` `instMulZeroClass` `factorization` `Finset.prod` `instCommMonoid` `setOf` `Squarefree` `instMonoid`	—	`primeFactors_prod` `prod_primeFactors_of_squarefree`
`prod_primeFactors_of_squarefree` 📖	mathematical	`Squarefree` `instMonoid`	`Finset.prod` `instCommMonoid` `primeFactors`	—	`toFinset_factors` `List.prod_toFinset` `Squarefree.nodup_primeFactorsList` `prod_primeFactorsList` `Squarefree.ne_zero` `instNontrivial`
`prod_primeFactors_sdiff_of_squarefree` 📖	mathematical	`Squarefree` `instMonoid` `Finset` `Finset.instHasSubset` `primeFactors`	`Finset.prod` `instCommMonoid` `Finset.instSDiff`	—	`symm` `IsEquiv.toSymm` `eq_isEquiv` `Finset.prod_pos` `instZeroLEOneClass` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `instNontrivial` `Prime.pos` `prime_of_mem_primeFactorsList` `List.mem_toFinset` `Finset.prod_sdiff` `prod_primeFactors_of_squarefree`
`sq_mul_squarefree` 📖	mathematical	—	`Monoid.toNatPow` `instMonoid` `Squarefree`	—	`zero_pow` `instCharZero` `instAtLeastTwoHAddOfNat` `mul_one` `squarefree_one` `sq_mul_squarefree_of_pos`
`sq_mul_squarefree_of_pos` 📖	mathematical	—	`Monoid.toNatPow` `instMonoid` `Squarefree`	—	`one_pow` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Unique.instSubsingleton` `Finset.max'_mem` `CanonicallyOrderedAdd.mul_pos` `instCanonicallyOrderedAdd` `IsStrictOrderedRing.noZeroDivisors` `instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `pow_pos_iff` `two_ne_zero` `isUnit_iff` `Finset.filter.congr_simp` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.mul_pf_right` `mul_pow` `lt_mul_of_one_lt_right` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `MulZeroClass.mul_zero` `MulZeroClass.zero_mul` `Finset.le_max'`
`sq_mul_squarefree_of_pos'` 📖	mathematical	—	`Monoid.toNatPow` `instMonoid` `Squarefree`	—	`sq_mul_squarefree_of_pos`
`squarefree_and_prime_pow_iff_prime` 📖	mathematical	—	`Squarefree` `instMonoid` `IsPrimePow` `instCommMonoidWithZero` `Prime`	—	`isPrimePow_nat_iff` `squarefree_pow_iff` `Prime.ne_one` `LT.lt.ne'` `pow_one` `Irreducible.squarefree` `Prime.isPrimePow`
`squarefree_iff_factorization_le_one` 📖	mathematical	—	`Squarefree` `instMonoid` `DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `instMulZeroClass` `Finsupp.instFunLike` `factorization`	—	`Squarefree.natFactorization_le_one` `squarefree_of_factorization_le_one`
`squarefree_iff_minSqFac` 📖	mathematical	—	`Squarefree` `instMonoid` `minSqFac`	—	`minSqFac_has_prop` `squarefree_iff_prime_squarefree`
`squarefree_iff_nodup_primeFactorsList` 📖	mathematical	—	`Squarefree` `instMonoid` `primeFactorsList`	—	`Unique.instSubsingleton` `instUniqueFactorizationMonoid` `UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors` `factors_eq`
`squarefree_iff_prime_squarefree` 📖	mathematical	—	`Squarefree` `instMonoid`	—	`squarefree_iff_irreducible_sq_not_dvd_of_exists_irreducible` `instWfDvdMonoid` `prime_two`
`squarefree_mul` 📖	mathematical	—	`Squarefree` `instMonoid`	—	`instIsCancelMulZero` `instDecompositionMonoidOfNonemptyGCDMonoid` `instNonemptyGCDMonoidOfNormalizedGCDMonoid` `instNonemptyNormalizedGCDMonoidOfUniqueFactorizationMonoid` `instUniqueFactorizationMonoid` `coprime_iff_isRelPrime`
`squarefree_mul_iff` 📖	mathematical	—	`Squarefree` `instMonoid`	—	`squarefree_mul_iff` `instIsCancelMulZero` `instDecompositionMonoidOfNonemptyGCDMonoid` `instNonemptyGCDMonoidOfNormalizedGCDMonoid` `instNonemptyNormalizedGCDMonoidOfUniqueFactorizationMonoid` `instUniqueFactorizationMonoid` `coprime_iff_isRelPrime`
`squarefree_of_factorization_le_one` 📖	mathematical	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `instMulZeroClass` `Finsupp.instFunLike` `factorization`	`Squarefree` `instMonoid`	—	`squarefree_iff_nodup_primeFactorsList` `List.nodup_iff_count_le_one` `primeFactorsList_count_eq`
`squarefree_pow_iff` 📖	mathematical	—	`Squarefree` `instMonoid` `Monoid.toNatPow`	—	`eq_or_ne` `zero_pow` `instNontrivial` `Squarefree.squarefree_of_dvd` `dvd_pow_self` `by_contradiction` `two_le_iff` `isUnit_iff` `sq` `pow_dvd_pow` `pow_one`
`squarefree_two` 📖	mathematical	—	`Squarefree` `instMonoid`	—	`squarefree_iff_nodup_primeFactorsList` `instCharZero` `instAtLeastTwoHAddOfNat` `primeFactorsList_two`
`sum_divisors_filter_squarefree` 📖	mathematical	—	`Finset.sum` `Finset.filter` `Squarefree` `instMonoid` `instDecidablePredSquarefree` `divisors` `Finset` `Finset.powerset` `Multiset.toFinset` `UniqueFactorizationMonoid.normalizedFactors` `instCommMonoidWithZero` `NormalizationMonoid.ofUniqueUnits` `Unique.instSubsingleton` `Units` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `unique_units` `instUniqueFactorizationMonoid` `Multiset.prod` `instCommMonoid` `Finset.val`	—	`Unique.instSubsingleton` `instUniqueFactorizationMonoid` `Finset.sum_eq_multiset_sum` `divisors_filter_squarefree` `Multiset.map_map`

Nat.Squarefree

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext_iff` 📖	—	`Squarefree` `Nat.instMonoid`	—	—	`Nat.eq_of_factorization_eq` `Squarefree.ne_zero` `Nat.instNontrivial` `Squarefree.natFactorization_le_one` `not_le` `Nat.Prime.dvd_iff_one_le_factorization` `not_iff_not` `Nat.factorization_eq_zero_of_not_prime`

Squarefree

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`natFactorization_le_one` 📖	mathematical	`Squarefree` `Nat.instMonoid`	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instFunLike` `Nat.factorization`	—	`eq_or_ne` `Nat.factorization_zero` `Nat.instCanonicallyOrderedAdd` `squarefree_iff_emultiplicity_le_one` `Nat.multiplicity_eq_factorization` `multiplicity_le_of_emultiplicity_le` `Nat.Prime.ne_one` `Nat.factorization_eq_zero_of_not_prime` `zero_le_one` `Nat.instZeroLEOneClass`
`nodup_primeFactorsList` 📖	mathematical	`Squarefree` `Nat.instMonoid`	`Nat.primeFactorsList`	—	`Nat.squarefree_iff_nodup_primeFactorsList` `ne_zero` `Nat.instNontrivial`

(root)

Definitions

Name	Category	Theorems
`Squarefree` 📖	MathDef	50 math math: `Nat.squarefree_and_prime_pow_iff_prime`, `UniqueFactorizationMonoid.squarefree_radical`, `Ideal.squarefree_span_singleton`, `Nat.sq_mul_squarefree_of_pos`, `Nat.sq_mul_squarefree`, `squarefree_one`, `Nat.squarefree_of_factorization_le_one`, `ArithmeticFunction.moebius_sq`, `Nat.squarefree_pow_iff`, `BoundingSieve.prodPrimes_squarefree`, `Polynomial.squarefree_cyclotomic`, `squarefree_iff_irreducible_sq_not_dvd_of_exists_irreducible`, `squarefree_iff_irreducible_sq_not_dvd_of_ne_zero`, `BoundingSieve.squarefree_of_dvd_prodPrimes`, `isRadical_iff_squarefree_or_zero`, `Irreducible.squarefree`, `Associated.squarefree_iff`, `isRadical_iff_squarefree_of_ne_zero`, `IsUnit.squarefree`, `ArithmeticFunction.moebius_ne_zero_iff_squarefree`, `Nat.sum_divisors_filter_squarefree`, `Int.squarefree_natAbs`, `IsRadical.squarefree`, `squarefree_iff_emultiplicity_le_one`, `Nat.squarefree_iff_nodup_primeFactorsList`, `BoundingSieve.squarefree_of_mem_divisors_prodPrimes`, `IsPrimitiveRoot.squarefree_minpoly_mod`, `squarefree_mul_iff`, `Int.squarefree_natCast`, `PerfectField.separable_iff_squarefree`, `irreducible_sq_not_dvd_iff_eq_zero_and_no_irreducibles_or_squarefree`, `exists_squarefree_dvd_pow_of_ne_zero`, `not_squarefree_zero`, `Prime.squarefree`, `Polynomial.Separable.squarefree`, `Nat.squarefree_two`, `Module.End.IsSemisimple.minpoly_squarefree`, `isReduced_zmod`, `Nat.squarefree_iff_minSqFac`, `Nat.squarefree_iff_prime_squarefree`, `squarefree_iff_no_irreducibles`, `Nat.prod_primeFactors_invOn_squarefree`, `UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors`, `Nat.squarefree_mul`, `Nat.divisors_filter_squarefree`, `Nat.sq_mul_squarefree_of_pos'`, `ArithmeticFunction.cardDistinctFactors_eq_cardFactors_iff_squarefree`, `Nat.squarefree_iff_factorization_le_one`, `Nat.squarefree_mul_iff`, `ArithmeticFunction.abs_moebius`

---

← Back to Index