Finsupp

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

Statistics

Metric	Count
Definitions factorization	1
Theorems associated_of_factorization_eq, factorization_eq_count, factorization_mul, factorization_one, factorization_pow, factorization_zero, support_factorization	7
Total	8

(root)

Definitions

Name	Category	Theorems
factorization 📖	CompOp	6 math math: factorization_pow, factorization_mul, factorization_zero, factorization_eq_count, support_factorization, factorization_one

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associated_of_factorization_eq 📖	mathematical	factorization	Associated MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero	—	UniqueFactorizationMonoid.associated_iff_normalizedFactors_eq_normalizedFactors
factorization_eq_count 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instFunLike factorization Multiset.count UniqueFactorizationMonoid.normalizedFactors	—	—
factorization_mul 📖	mathematical	—	factorization MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid	—	UniqueFactorizationMonoid.normalizedFactors_mul map_add AddMonoidHomClass.toAddHomClass AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass
factorization_one 📖	mathematical	—	factorization MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instZero	—	UniqueFactorizationMonoid.normalizedFactors_one map_zero AddMonoidHomClass.toZeroHomClass AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass
factorization_pow 📖	mathematical	—	factorization Monoid.toNatPow MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instNatSMul Nat.instAddMonoid	—	Finsupp.ext UniqueFactorizationMonoid.normalizedFactors_pow map_nsmul AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass
factorization_zero 📖	mathematical	—	factorization MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero Finsupp Nat.instMulZeroClass Finsupp.instZero	—	UniqueFactorizationMonoid.normalizedFactors_zero map_zero AddMonoidHomClass.toZeroHomClass AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass
support_factorization 📖	mathematical	—	Finsupp.support MulZeroClass.toZero Nat.instMulZeroClass factorization Multiset.toFinset UniqueFactorizationMonoid.normalizedFactors	—	—

---

← Back to Index