Ideal

📁 Source: Mathlib/Algebra/Order/Group/Ideal.lean

Statistics

Metric	Count
Definitions	0
Theorems fg_of_wellQuasiOrderedLE, instWellFoundedGT, fg_of_wellQuasiOrderedLE, instWellFoundedGT	4
Total	4

AddSemigroupIdeal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fg_of_wellQuasiOrderedLE 📖	mathematical	—	FG AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	Set.isPWO_of_wellQuasiOrderedLE IsAntichain.finite_of_partiallyWellOrderedOn setOf_minimal_antichain Set.IsPWO.mono setOf_minimal_subset SubAddAction.ext SetLike.mem_coe mem_closure'' Set.IsPWO.exists_le_minimal le_iff_exists_add' SubAddAction.vadd_mem
instWellFoundedGT 📖	mathematical	—	WellFoundedGT AddSemigroupIdeal AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Preorder.toLT PartialOrder.toPreorder SubAddAction.instPartialOrder Add.toVAdd	—	wellFoundedGT_iff_monotone_chain_condition fg_iff fg_of_wellQuasiOrderedLE SetLike.mem_coe SubAddAction.mem_iSup subset_closure LE.le.antisymm OrderHom.mono LE.le.trans le_iSup mem_closure'' add_mem Finset.le_sup Function.sometimes_spec

SemigroupIdeal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fg_of_wellQuasiOrderedLE 📖	mathematical	—	FG MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	Set.isPWO_of_wellQuasiOrderedLE IsAntichain.finite_of_partiallyWellOrderedOn setOf_minimal_antichain Set.IsPWO.mono setOf_minimal_subset SubMulAction.ext Set.IsPWO.exists_le_minimal le_iff_exists_mul' SubMulAction.smul_mem
instWellFoundedGT 📖	mathematical	—	WellFoundedGT SemigroupIdeal MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Preorder.toLT PartialOrder.toPreorder SubMulAction.instPartialOrder	—	wellFoundedGT_iff_monotone_chain_condition fg_iff fg_of_wellQuasiOrderedLE subset_closure LE.le.antisymm OrderHom.mono LE.le.trans le_iSup mem_closure'' mul_mem Finset.le_sup Function.sometimes_spec

---

← Back to Index