Induction

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

Statistics

Metric	Count
Definitions recOnMul, recOnPosPrimePosCoprime, recOnPrimeCoprime, recOnPrimePow	4
Theorems multiplicative_factorization, multiplicative_factorization', prime_composite_induction, induction_on_primes	4
Total	8

Nat

Definitions

Name	Category	Theorems
recOnMul 📖	CompOp	—
recOnPosPrimePosCoprime 📖	CompOp	—
recOnPrimeCoprime 📖	CompOp	—
recOnPrimePow 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
multiplicative_factorization 📖	mathematical	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid MulOne.toOne	Finsupp.prod MulZeroClass.toZero instMulZeroClass factorization Monoid.toNatPow instMonoid	—	Prime.factorization_pow Finsupp.prod_single_index pow_zero factorization_zero instIsEmptyFalse factorization_one left_ne_zero_of_mul right_ne_zero_of_mul factorization_mul_of_coprime Finsupp.prod_add_index_of_disjoint Coprime.disjoint_primeFactors
multiplicative_factorization' 📖	mathematical	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid MulOne.toOne	Finsupp.prod MulZeroClass.toZero instMulZeroClass factorization Monoid.toNatPow instMonoid	—	eq_or_ne factorization_zero multiplicative_factorization
prime_composite_induction 📖	—	—	—	—	induction_on_primes MulZeroClass.mul_zero zero_add mul_one Prime.two_le

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
induction_on_primes 📖	—	—	—	—	pow_zero one_mul mul_assoc

---

← Back to Index