Factors

📁 Source: Mathlib/Tactic/Simproc/Factors.lean

Statistics

Metric	Count
Definitions Factors, Factors, FactorsHelper, evalPrimeFactorsList, primeFactorsList_ofNat	5
Theorems cons, cons_of_le, cons_self, nil, primeFactorsList_eq, singleton, singleton_self	7
Total	12

CategoryTheory.MonoOver

Definitions

Name	Category	Theorems
Factors 📖	MathDef	3 math math: CategoryTheory.Subobject.factors_iff, CategoryTheory.Subobject.mk_factors_iff, factors_congr

CategoryTheory.Subobject

Definitions

Name	Category	Theorems
Factors 📖	MathDef	32 math math: factors_iff, factors_add, inf_arrow_factors_right, finset_sup_factors, mk_factors_iff, CategoryTheory.Limits.kernelSubobject_factors, factors_right_of_inf_factors, bot_factors_iff_zero, CategoryTheory.Limits.pullback_factors_iff, factors_comp_arrow, factors_self, factors_right_of_factors_add, inf_factors, CategoryTheory.Limits.kernelSubobject_factors_iff, CategoryTheory.Limits.equalizerSubobject_factors_iff, factors_of_factors_right, finset_inf_factors, mk_factors_self, CategoryTheory.Limits.pullback_factors, inf_arrow_factors_left, top_factors, factors_left_of_factors_add, factors_left_of_inf_factors, sup_factors_of_factors_left, CategoryTheory.ObjectProperty.IsStrongGenerator.exists_of_subobject_ne_top, sup_factors_of_factors_right, factors_zero, finset_inf_arrow_factors, AlgebraicTopology.DoldKan.factors_normalizedMooreComplex_PInfty, CategoryTheory.Limits.equalizerSubobject_factors, factors_of_le, CategoryTheory.Limits.imageSubobject_factors_comp_self

Mathlib.Meta.Simproc

Definitions

Name	Category	Theorems
FactorsHelper 📖	MathDef	6 math math: FactorsHelper.cons_of_le, FactorsHelper.cons_self, FactorsHelper.cons, FactorsHelper.nil, FactorsHelper.singleton_self, FactorsHelper.singleton
evalPrimeFactorsList 📖	CompOp	—

Mathlib.Meta.Simproc.FactorsHelper

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cons 📖	mathematical	Mathlib.Meta.NormNum.IsNat Nat.instAddMonoidWithOne Nat.minFac Mathlib.Meta.Simproc.FactorsHelper	Mathlib.Meta.Simproc.FactorsHelper	—	cons_of_le LT.lt.le Mathlib.Meta.NormNum.IsNat.out
cons_of_le 📖	mathematical	Mathlib.Meta.NormNum.IsNat Nat.instAddMonoidWithOne Nat.minFac Mathlib.Meta.Simproc.FactorsHelper	Mathlib.Meta.Simproc.FactorsHelper	—	Nat.prime_def_minFac le_trans Nat.Prime.two_le Mathlib.Meta.NormNum.IsNat.out Nat.cast_id
cons_self 📖	mathematical	Mathlib.Meta.NormNum.IsNat Nat.instAddMonoidWithOne Mathlib.Meta.Simproc.FactorsHelper	Mathlib.Meta.Simproc.FactorsHelper	—	cons_of_le le_rfl Nat.prime_def_minFac
nil 📖	mathematical	—	Mathlib.Meta.Simproc.FactorsHelper	—	—
primeFactorsList_eq 📖	mathematical	Mathlib.Meta.Simproc.FactorsHelper	Nat.primeFactorsList	—	Nat.prime_two List.IsChain.tail List.Perm.eq_of_pairwise' List.SortedLE.pairwise Nat.primeFactorsList_sorted Nat.primeFactorsList_unique
singleton 📖	mathematical	Mathlib.Meta.NormNum.IsNat Nat.instAddMonoidWithOne Nat.minFac	Mathlib.Meta.Simproc.FactorsHelper	—	cons mul_one nil
singleton_self 📖	mathematical	—	Mathlib.Meta.Simproc.FactorsHelper	—	cons_self mul_one nil

Nat

Definitions

Name	Category	Theorems
primeFactorsList_ofNat 📖	CompOp	—

---

← Back to Index