Moebius

📁 Source: Mathlib/NumberTheory/ArithmeticFunction/Moebius.lean

Statistics

Metric	Count
Definitions `termμ`, `instInvertibleNatToArithmeticFunctionZeta`, `moebius`, `zetaUnit`	4
Theorems `prodPrimeFactors_one_add_of_squarefree`, `prodPrimeFactors_one_sub_of_squarefree`, `abs_moebius`, `abs_moebius_eq_one_of_squarefree`, `abs_moebius_le_one`, `coe_moebius_mul_coe_zeta`, `coe_zetaUnit`, `coe_zeta_mul_coe_moebius`, `coe_zeta_mul_moebius`, `inv_zetaUnit`, `isMultiplicative_moebius`, `moebius_apply_isPrimePow_not_prime`, `moebius_apply_of_squarefree`, `moebius_apply_one`, `moebius_apply_prime`, `moebius_apply_prime_pow`, `moebius_eq_or`, `moebius_eq_zero_of_not_squarefree`, `moebius_mul_coe_zeta`, `moebius_ne_zero_iff_eq_or`, `moebius_ne_zero_iff_squarefree`, `moebius_sq`, `moebius_sq_eq_one_of_squarefree`, `prod_eq_iff_prod_pow_moebius_eq`, `prod_eq_iff_prod_pow_moebius_eq_of_nonzero`, `prod_eq_iff_prod_pow_moebius_eq_on`, `prod_eq_iff_prod_pow_moebius_eq_on_of_nonzero`, `sum_eq_iff_sum_mul_moebius_eq`, `sum_eq_iff_sum_mul_moebius_eq_on`, `sum_eq_iff_sum_smul_moebius_eq`, `sum_eq_iff_sum_smul_moebius_eq_on`, `sum_eq_iff_sum_smul_moebius_eq_on'`	32
Total	36

ArithmeticFunction

Definitions

Name	Category	Theorems
`instInvertibleNatToArithmeticFunctionZeta` 📖	CompOp	—
`moebius` 📖	CompOp	41 math math: `coe_moebius_mul_coe_zeta`, `moebius_eq_or`, `moebius_ne_zero_iff_eq_or`, `LSeries_zeta_mul_Lseries_moebius`, `prod_eq_iff_prod_pow_moebius_eq`, `moebius_sq`, `moebius_apply_one`, `not_LSeriesSummable_moebius_at_one`, `moebius_mul_coe_zeta`, `moebius_apply_prime_pow`, `moebius_eq_zero_of_not_squarefree`, `prod_eq_iff_prod_pow_moebius_eq_on_of_nonzero`, `moebius_apply_of_squarefree`, `DirichletCharacter.LSeries.mul_mu_eq_one`, `moebius_apply_prime`, `coe_zeta_mul_coe_moebius`, `sum_eq_iff_sum_smul_moebius_eq`, `sum_eq_iff_sum_mul_moebius_eq_on`, `sum_eq_iff_sum_mul_moebius_eq`, `log_mul_moebius_eq_vonMangoldt`, `moebius_sq_eq_one_of_squarefree`, `LSeries_one_mul_Lseries_moebius`, `moebius_mul_log_eq_vonMangoldt`, `abs_moebius_eq_one_of_squarefree`, `Polynomial.cyclotomic_eq_prod_X_pow_sub_one_pow_moebius`, `LSeriesSummable_moebius_iff`, `sum_moebius_mul_log_eq`, `isMultiplicative_moebius`, `prod_eq_iff_prod_pow_moebius_eq_on`, `inv_zetaUnit`, `coe_zeta_mul_moebius`, `DirichletCharacter.convolution_mul_moebius`, `Nat.moebius_eq`, `abs_moebius_le_one`, `sum_eq_iff_sum_smul_moebius_eq_on'`, `prod_eq_iff_prod_pow_moebius_eq_of_nonzero`, `IsMultiplicative.prodPrimeFactors_one_sub_of_squarefree`, `sum_eq_iff_sum_smul_moebius_eq_on`, `moebius_apply_isPrimePow_not_prime`, `abscissaOfAbsConv_moebius`, `abs_moebius`
`zetaUnit` 📖	CompOp	2 math math: `inv_zetaUnit`, `coe_zetaUnit`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_moebius` 📖	mathematical	—	`abs` `instLatticeInt` `Int.instAddGroup` `DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `instFunLikeNat` `moebius` `Squarefree` `Nat.instMonoid` `Nat.instDecidablePredSquarefree`	—	`abs_moebius_eq_one_of_squarefree` `moebius_eq_zero_of_not_squarefree` `abs_zero` `Int.instAddLeftMono`
`abs_moebius_eq_one_of_squarefree` 📖	mathematical	`Squarefree` `Nat.instMonoid`	`abs` `instLatticeInt` `Int.instAddGroup` `DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `instFunLikeNat` `moebius`	—	`moebius_apply_of_squarefree` `abs_pow` `IsStrictOrderedRing.toIsOrderedRing` `Int.instIsStrictOrderedRing` `abs_neg` `abs_one` `one_pow`
`abs_moebius_le_one` 📖	mathematical	—	`abs` `instLatticeInt` `Int.instAddGroup` `DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `instFunLikeNat` `moebius`	—	`abs_moebius` `Int.instZeroLEOneClass`
`coe_moebius_mul_coe_zeta` 📖	mathematical	—	`ArithmeticFunction` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `instMul` `Ring.toSemiring` `ofInt` `moebius` `natToArithmeticFunction` `zeta` `one` `AddMonoidWithOne.toOne`	—	`coe_coe` `intCoe_mul` `moebius_mul_coe_zeta` `intCoe_one`
`coe_zetaUnit` 📖	mathematical	—	`Units.val` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instMonoid` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `zetaUnit` `natToArithmeticFunction` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `zeta`	—	—
`coe_zeta_mul_coe_moebius` 📖	mathematical	—	`ArithmeticFunction` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddGroupWithOne.toAddGroup` `instMul` `Ring.toSemiring` `natToArithmeticFunction` `zeta` `ofInt` `moebius` `one` `AddMonoidWithOne.toOne`	—	`coe_coe` `intCoe_mul` `coe_zeta_mul_moebius` `intCoe_one`
`coe_zeta_mul_moebius` 📖	mathematical	—	`ArithmeticFunction` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `instMul` `Int.instSemiring` `natToArithmeticFunction` `zeta` `moebius` `one` `AddMonoidWithOne.toOne`	—	`mul_comm` `moebius_mul_coe_zeta`
`inv_zetaUnit` 📖	mathematical	—	`Units.val` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instMonoid` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Units` `Units.instInv` `zetaUnit` `ofInt` `Ring.toAddGroupWithOne` `CommRing.toRing` `moebius`	—	—
`isMultiplicative_moebius` 📖	mathematical	—	`IsMultiplicative` `Semiring.toMonoidWithZero` `Int.instSemiring` `moebius`	—	`IsMultiplicative.iff_ne_zero` `moebius_apply_of_squarefree` `Unique.instSubsingleton` `cardFactors_one` `pow_zero` `Nat.squarefree_mul` `cardFactors_mul` `pow_add` `ite_zero_mul_ite_zero`
`moebius_apply_isPrimePow_not_prime` 📖	mathematical	`IsPrimePow` `Nat.instCommMonoidWithZero` `Nat.Prime`	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `instFunLikeNat` `moebius`	—	`isPrimePow_nat_iff` `moebius_apply_prime_pow` `LT.lt.ne'` `pow_one`
`moebius_apply_of_squarefree` 📖	mathematical	`Squarefree` `Nat.instMonoid`	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `instFunLikeNat` `moebius` `Monoid.toNatPow` `Int.instMonoid` `Nat.instMulZeroClass` `cardFactors`	—	—
`moebius_apply_one` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `instFunLikeNat` `moebius`	—	`moebius_apply_of_squarefree` `Unique.instSubsingleton` `cardFactors_one` `pow_zero`
`moebius_apply_prime` 📖	mathematical	`Nat.Prime`	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `instFunLikeNat` `moebius`	—	`moebius_apply_of_squarefree` `Irreducible.squarefree` `cardFactors_apply_prime` `pow_one`
`moebius_apply_prime_pow` 📖	mathematical	`Nat.Prime`	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `instFunLikeNat` `moebius` `Monoid.toNatPow` `Nat.instMonoid`	—	`pow_one` `moebius_apply_prime` `moebius_eq_zero_of_not_squarefree` `Nat.squarefree_pow_iff` `Nat.Prime.ne_one` `not_and_or`
`moebius_eq_or` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `instFunLikeNat` `moebius`	—	`neg_one_pow_eq_or`
`moebius_eq_zero_of_not_squarefree` 📖	mathematical	`Squarefree` `Nat.instMonoid`	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `instFunLikeNat` `moebius`	—	—
`moebius_mul_coe_zeta` 📖	mathematical	—	`ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `instMul` `Int.instSemiring` `moebius` `natToArithmeticFunction` `zeta` `one` `AddMonoidWithOne.toOne`	—	`ext` `coe_mul_zeta_apply` `Nat.sum_divisors_prime_pow` `Finset.sum_range_succ'` `Finset.sum_congr` `moebius_apply_prime_pow` `Finset.sum_ite_eq'` `pow_zero` `moebius_apply_of_squarefree` `Unique.instSubsingleton` `cardFactors_one` `neg_add_cancel` `one_apply_ne` `Nat.instIsMulTorsionFree` `Nat.Prime.ne_one` `LT.lt.ne'` `map_zero` `Nat.divisorsAntidiagonal_one` `Nat.cast_ite` `Nat.cast_zero` `Nat.cast_one` `mul_ite` `MulZeroClass.mul_zero` `mul_one` `Finset.sum_singleton` `IsMultiplicative.map_mul_of_coprime` `IsMultiplicative.mul` `isMultiplicative_moebius` `IsMultiplicative.natCast` `isMultiplicative_zeta` `isMultiplicative_one`
`moebius_ne_zero_iff_eq_or` 📖	mathematical	—	`DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `instFunLikeNat` `moebius`	—	`moebius_eq_or`
`moebius_ne_zero_iff_squarefree` 📖	mathematical	—	`Squarefree` `Nat.instMonoid`	—	`Mathlib.Tactic.Contrapose.contrapose₂` `moebius_eq_zero_of_not_squarefree` `moebius_apply_of_squarefree` `isReduced_of_noZeroDivisors` `IsStrictOrderedRing.noZeroDivisors` `Int.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `Int.instNontrivial`
`moebius_sq` 📖	mathematical	—	`Monoid.toNatPow` `Int.instMonoid` `DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `instFunLikeNat` `moebius` `Squarefree` `Nat.instMonoid` `Nat.instDecidablePredSquarefree`	—	`moebius_sq_eq_one_of_squarefree` `moebius_eq_zero_of_not_squarefree` `zero_pow` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat`
`moebius_sq_eq_one_of_squarefree` 📖	mathematical	`Squarefree` `Nat.instMonoid`	`Monoid.toNatPow` `Int.instMonoid` `DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `instFunLikeNat` `moebius`	—	`moebius_apply_of_squarefree` `pow_mul` `mul_comm` `neg_one_sq` `one_pow`
`prod_eq_iff_prod_pow_moebius_eq` 📖	mathematical	—	`Finset.prod` `CommGroup.toCommMonoid` `Nat.divisors` `Nat.divisorsAntidiagonal` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `CommGroup.toGroup` `DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `instFunLikeNat` `moebius`	—	`sum_eq_iff_sum_smul_moebius_eq`
`prod_eq_iff_prod_pow_moebius_eq_of_nonzero` 📖	mathematical	—	`Finset.prod` `CommMonoidWithZero.toCommMonoid` `CommGroupWithZero.toCommMonoidWithZero` `Nat.divisors` `Nat.divisorsAntidiagonal` `DivInvMonoid.toZPow` `GroupWithZero.toDivInvMonoid` `CommGroupWithZero.toGroupWithZero` `DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `instFunLikeNat` `moebius`	—	`Units.coeHom_apply` `map_prod` `MonoidHom.instMonoidHomClass` `Units.val_mk0` `Finset.prod_congr` `Nat.pos_of_mem_divisors` `prod_eq_iff_prod_pow_moebius_eq` `Nat.snd_mem_divisors_of_mem_antidiagonal` `Units.val_zpow_eq_zpow_val`
`prod_eq_iff_prod_pow_moebius_eq_on` 📖	mathematical	`Set` `Set.instMembership`	`Finset.prod` `CommGroup.toCommMonoid` `Nat.divisors` `Nat.divisorsAntidiagonal` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `CommGroup.toGroup` `DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `instFunLikeNat` `moebius`	—	`sum_eq_iff_sum_smul_moebius_eq_on`
`prod_eq_iff_prod_pow_moebius_eq_on_of_nonzero` 📖	mathematical	`Set` `Set.instMembership`	`Finset.prod` `CommMonoidWithZero.toCommMonoid` `CommGroupWithZero.toCommMonoidWithZero` `Nat.divisors` `Nat.divisorsAntidiagonal` `DivInvMonoid.toZPow` `GroupWithZero.toDivInvMonoid` `CommGroupWithZero.toGroupWithZero` `DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `instFunLikeNat` `moebius`	—	`Units.coeHom_apply` `map_prod` `MonoidHom.instMonoidHomClass` `Units.val_mk0` `Finset.prod_congr` `Nat.pos_of_mem_divisors` `prod_eq_iff_prod_pow_moebius_eq_on` `Nat.snd_mem_divisors_of_mem_antidiagonal` `Units.val_zpow_eq_zpow_val`
`sum_eq_iff_sum_mul_moebius_eq` 📖	mathematical	—	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Nat.divisors` `Nat.divisorsAntidiagonal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `instFunLikeNat` `moebius`	—	`sum_eq_iff_sum_smul_moebius_eq` `Finset.sum_congr` `zsmul_eq_mul`
`sum_eq_iff_sum_mul_moebius_eq_on` 📖	mathematical	`Set` `Set.instMembership`	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Nat.divisors` `Nat.divisorsAntidiagonal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `instFunLikeNat` `moebius`	—	`sum_eq_iff_sum_smul_moebius_eq_on` `Finset.sum_congr` `zsmul_eq_mul`
`sum_eq_iff_sum_smul_moebius_eq` 📖	mathematical	—	`Finset.sum` `AddCommGroup.toAddCommMonoid` `Nat.divisors` `Nat.divisorsAntidiagonal` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `instFunLikeNat` `moebius`	—	`ext_iff` `Finset.sum_congr` `Nat.divisors_zero` `instIsEmptyFalse` `map_zero` `coe_zeta_smul_apply` `LT.lt.ne'` `Nat.pos_of_mem_divisors` `moebius_mul_coe_zeta` `one_smul` `coe_zeta_mul_moebius` `Nat.divisorsAntidiagonal_zero` `Nat.snd_mem_divisors_of_mem_antidiagonal`
`sum_eq_iff_sum_smul_moebius_eq_on` 📖	mathematical	`Set` `Set.instMembership`	`Finset.sum` `AddCommGroup.toAddCommMonoid` `Nat.divisors` `Nat.divisorsAntidiagonal` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `instFunLikeNat` `moebius`	—	`Nat.sum_divisorsAntidiagonal'` `sum_eq_iff_sum_smul_moebius_eq` `Finset.sum_congr` `Nat.pos_of_mem_divisors` `Nat.dvd_of_mem_divisors`
`sum_eq_iff_sum_smul_moebius_eq_on'` 📖	mathematical	`Set` `Set.instMembership`	`Finset.sum` `AddCommGroup.toAddCommMonoid` `Nat.divisors` `Nat.divisorsAntidiagonal` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `instFunLikeNat` `moebius`	—	`Mathlib.Tactic.Contrapose.contrapose₂` `nonpos_iff_eq_zero` `Nat.instCanonicallyOrderedAdd` `sum_eq_iff_sum_smul_moebius_eq_on`

ArithmeticFunction.IsMultiplicative

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prodPrimeFactors_one_add_of_squarefree` 📖	mathematical	`ArithmeticFunction.IsMultiplicative` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Squarefree` `Nat.instMonoid`	`Finset.prod` `CommSemiring.toCommMonoid` `Nat.primeFactors` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `ArithmeticFunction.instFunLikeNat` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Nat.divisors`	—	`ArithmeticFunction.prodPrimeFactors_apply` `Squarefree.ne_zero` `Nat.instNontrivial` `Finset.prod_congr` `ArithmeticFunction.zeta_apply_ne` `Nat.Prime.ne_zero` `Nat.prime_of_mem_primeFactorsList` `List.mem_toFinset` `Nat.cast_one` `prodPrimeFactors_add_of_squarefree` `natCast` `ArithmeticFunction.isMultiplicative_zeta` `ArithmeticFunction.coe_zeta_mul_apply`
`prodPrimeFactors_one_sub_of_squarefree` 📖	mathematical	`ArithmeticFunction.IsMultiplicative` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Squarefree` `Nat.instMonoid`	`Finset.prod` `CommRing.toCommMonoid` `Nat.primeFactors` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `DFunLike.coe` `ArithmeticFunction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ArithmeticFunction.instFunLikeNat` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Nat.divisors` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddGroupWithOne.toIntCast` `Int.instCommRing` `ArithmeticFunction.moebius`	—	`Finset.prod_congr` `ArithmeticFunction.pmul_apply` `ArithmeticFunction.intCoe_apply` `ArithmeticFunction.moebius_apply_prime` `Nat.prime_of_mem_primeFactorsList` `List.mem_toFinset` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_neg` `Mathlib.Meta.NormNum.isintCast` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `prodPrimeFactors_one_add_of_squarefree` `pmul` `intCast` `ArithmeticFunction.isMultiplicative_moebius` `Finset.sum_congr`

ArithmeticFunction.Moebius

Definitions

Name	Category	Theorems
`termμ` 📖	CompOp	—

---

← Back to Index