Moebius

📁 Source: Mathlib/RingTheory/UniqueFactorizationDomain/Moebius.lean

Statistics

Metric	Count
Definitions moebius	1
Theorems moebius_eq, moebius_eq, moebius_mul, moebius_eq, moebius_eq, moebius_eq, moebius_of_not_squarefree, moebius_one, moebius_zero	9
Total	10

Associated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
moebius_eq 📖	mathematical	Associated MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero	UniqueFactorizationMonoid.moebius	—	UniqueFactorizationMonoid.moebius.eq_1 squarefree_iff card_factors_eq

Irreducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
moebius_eq 📖	mathematical	Irreducible MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero	UniqueFactorizationMonoid.moebius	—	Squarefree.moebius_eq squarefree UniqueFactorizationMonoid.card_factors_of_irreducible pow_one

IsRelPrime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
moebius_mul 📖	mathematical	IsRelPrime MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero	UniqueFactorizationMonoid.moebius MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass	—	subsingleton_or_nontrivial UniqueFactorizationMonoid.moebius_one one_mul squarefree_mul_iff UniqueFactorizationMonoid.toIsCancelMulZero instDecompositionMonoidOfNonemptyGCDMonoid instNonemptyGCDMonoidOfNormalizedGCDMonoid instNonemptyNormalizedGCDMonoidOfUniqueFactorizationMonoid Squarefree.moebius_eq Multiset.card_eq_card_of_rel UniqueFactorizationMonoid.factors_mul Squarefree.ne_zero Multiset.card_add pow_add UniqueFactorizationMonoid.moebius_of_not_squarefree Squarefree.of_mul_right MulZeroClass.mul_zero Squarefree.of_mul_left MulZeroClass.zero_mul

IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
moebius_eq 📖	mathematical	IsUnit MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero	UniqueFactorizationMonoid.moebius	—	Associated.moebius_eq associated_one_iff_isUnit UniqueFactorizationMonoid.moebius_one

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
moebius_eq 📖	mathematical	—	UniqueFactorizationMonoid.moebius instCommMonoidWithZero instUniqueFactorizationMonoid DFunLike.coe ArithmeticFunction MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing ArithmeticFunction.instFunLikeNat ArithmeticFunction.moebius	—	instUniqueFactorizationMonoid UniqueFactorizationMonoid.moebius.eq_1 Unique.instSubsingleton UniqueFactorizationMonoid.factors_eq_normalizedFactors factors_eq

Squarefree

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
moebius_eq 📖	mathematical	Squarefree MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero	UniqueFactorizationMonoid.moebius Monoid.toNatPow Int.instMonoid Multiset.card UniqueFactorizationMonoid.factors	—	—

UniqueFactorizationMonoid

Definitions

Name	Category	Theorems
moebius 📖	CompOp	9 math math: IsRelPrime.moebius_mul, moebius_one, Irreducible.moebius_eq, Associated.moebius_eq, moebius_of_not_squarefree, moebius_zero, IsUnit.moebius_eq, Nat.moebius_eq, Squarefree.moebius_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
moebius_of_not_squarefree 📖	mathematical	Squarefree MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero	moebius	—	—
moebius_one 📖	mathematical	—	moebius MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero	—	Squarefree.moebius_eq factors_one pow_zero
moebius_zero 📖	mathematical	—	moebius MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero	—	moebius_of_not_squarefree

---

← Back to Index