factors

📁 Source: MathlibTest/factors.lean

Statistics

Metric	Count
Definitions factors, factors, factors, factors	4
Theorems factors, factors, factors	3
Total	7

Associates

Definitions

Name	Category	Theorems
factors 📖	CompOp	48 math math: dvd_count_pow, FractionalIdeal.finprod_heightOneSpectrum_factorization_principal, prime_pow_dvd_iff_le, factors_mul, finite_factors, IsDedekindDomain.HeightOneSpectrum.intValuation_if_neg, FractionalIdeal.count_well_defined, eq_pow_count_factors_of_dvd_pow, IsDedekindDomain.HeightOneSpectrum.intValuationDef_if_neg, pow_factors, count_self, count_of_coprime, FractionalIdeal.finprod_heightOneSpectrum_factorization, factors_zero, FractionalIdeal.count_ne_zero, factors_subsingleton, factors_mk, factors_le, count_le_count_of_le, factors_prime_pow, count_pow, factors_mono, factors_eq_some_iff_ne_zero, prod_factors, Ideal.finite_mulSupport_coe, mem_factors_iff_dvd, count_mul_of_coprime', factors_eq_top_iff_zero, count_factors_eq_find_of_dvd_pow, IsDedekindDomain.HeightOneSpectrum.intValuation_def, Ideal.count_associates_eq, count_mul, Ideal.finprod_count, count_eq_zero_of_ne, Ideal.finprod_heightOneSpectrum_factorization_coe, prime_pow_le_iff_le_bcount, FractionalIdeal.finite_factors', count_associates_factors_eq, mem_factors_of_dvd, Ideal.count_associates_eq', factors_prod, count_mul_of_coprime, factors_self, FractionalIdeal.finprod_heightOneSpectrum_factorization_principal_fraction, Ideal.finprod_not_dvd, factors_one, Ideal.finite_mulSupport_inv, FractionalIdeal.count_coe

CategoryTheory.Injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
factors 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—

CategoryTheory.Projective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
factors 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—

IsAlgClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
factors 📖	mathematical	—	Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	splits

PrincipalIdealRing

Definitions

Name	Category	Theorems
factors 📖	CompOp	1 math math: factors_spec

Profinite.NobelingProof

Definitions

Name	Category	Theorems
factors 📖	CompOp	5 math math: factors_prod_eq_basis_of_ne, e_mem_of_eq_true, one_sub_e_mem_of_false, factors_prod_eq_basis, factors_prod_eq_basis_of_eq

UniqueFactorizationMonoid

Definitions

Name	Category	Theorems
factors 📖	CompOp	32 math math: factors_one, factors_eq_normalizedFactors, Submodule.isInternal_prime_power_torsion_of_pid, Ideal.Factors.fact_ramificationIdx_neZero, factors_eq_singleton_of_irreducible, factors_pow, exists_mem_factors, Submodule.isInternal_prime_power_torsion_of_is_torsion_by_ideal, factors_pow_count_prod, factors_rel_of_associated, factors_pos, Ideal.Factors.isScalarTower, Associates.map_subtype_coe_factors', Associated.card_factors_eq, Ideal.Factors.liesOver, factors_prod, Ideal.Factors.finrank_pow_ramificationIdx, Ideal.factors_span_eq, Submodule.isInternal_prime_power_torsion, Ideal.IsDedekindDomain.ramificationIdx_eq_factors_count, Ideal.Factors.finiteDimensional_quotient_pow, card_factors_of_irreducible, Ideal.Factors.isPrime, factors_zero, factors_mul, factors_of_isUnit, Ideal.Factors.piQuotientEquiv_mk, factors_eq_zero, IsDedekindDomain.quotientEquivPiFactors_mk, Squarefree.moebius_eq, Ideal.Factors.piQuotientEquiv_map, exists_mem_factors_of_dvd

---

← Back to Index