Irreducible

📁 Source: Mathlib/Algebra/AffineMonoid/Irreducible.lean

Statistics

Metric	Count
Definitions	0
Theorems finite_addIrreducible_mem_addSubmonoidClosure, closure_addIrreducible, finite_irreducible_mem_submonoidClosure, closure_irreducible, addIrreducible_mem_addSubmonoidClosure_subset, addIrreducible_subset_of_addSubmonoidClosure_eq_top, finite_addIrreducible, finite_irreducible, irreducible_mem_submonoidClosure_subset, irreducible_subset_of_submonoidClosure_eq_top	10
Total	10

AddSubmonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_addIrreducible 📖	mathematical	—	closure AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid setOf AddIrreducible Top.top AddSubmonoid instTop	—	exists_minimal_closure_eq_top HasSubset.Subset.antisymm Set.instAntisymmSubset addIrreducible_subset_of_addSubmonoidClosure_eq_top eq_or_ne Finset.mem_sdiff Finset.mem_singleton Finset.coe_sdiff Finset.coe_singleton closure_sdiff_singleton_zero Finset.sdiff_subset addIrreducible_iff isAddUnit_iff_eq_zero mem_closure_finset mem_top Finset.sdiff_singleton_eq_erase Finset.add_sum_erase add_nsmul add_assoc add_comm zero_nsmul zero_add Set.singleton_subset_iff AddMemClass.add_mem AddSubmonoidClass.toAddMemClass instAddSubmonoidClass sum_mem nsmul_mem subset_closure Set.mem_diff SetLike.mem_coe Set.mem_singleton_iff closure_sdiff_eq_closure Finset.sum_eq_zero one_nsmul add_eq_left AddLeftCancelSemigroup.toIsLeftCancelAdd AddLeftCancelMonoid.add_eq_zero Finset.sum_eq_zero_iff add_zero add_left_comm left_eq_add

AddSubmonoid.FG

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_addIrreducible_mem_addSubmonoidClosure 📖	mathematical	AddSubmonoid.FG AddCommMonoid.toAddMonoid	Set.Finite setOf AddSubmonoid AddMonoid.toAddZeroClass SetLike.instMembership AddSubmonoid.instSetLike AddIrreducible	—	Set.Finite.subset Finset.finite_toSet addIrreducible_mem_addSubmonoidClosure_subset

Submonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_irreducible 📖	mathematical	—	closure Monoid.toMulOneClass CommMonoid.toMonoid CancelCommMonoid.toCommMonoid setOf Irreducible Top.top Submonoid instTop	—	exists_minimal_closure_eq_top HasSubset.Subset.antisymm Set.instAntisymmSubset irreducible_subset_of_submonoidClosure_eq_top eq_or_ne Finset.coe_sdiff Finset.coe_singleton closure_sdiff_singleton_one Finset.sdiff_subset mem_closure_finset mem_top Finset.sdiff_singleton_eq_erase Finset.mul_prod_erase pow_add mul_assoc mul_comm pow_zero one_mul Set.singleton_subset_iff MulMemClass.mul_mem SubmonoidClass.toMulMemClass instSubmonoidClass prod_mem pow_mem subset_closure closure_sdiff_eq_closure Finset.prod_eq_one pow_one LeftCancelSemigroup.toIsLeftCancelMul mul_one mul_left_comm

Submonoid.FG

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_irreducible_mem_submonoidClosure 📖	mathematical	Submonoid.FG CommMonoid.toMonoid	Set.Finite setOf Submonoid Monoid.toMulOneClass SetLike.instMembership Submonoid.instSetLike Irreducible	—	Set.Finite.subset Finset.finite_toSet irreducible_mem_submonoidClosure_subset

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addIrreducible_mem_addSubmonoidClosure_subset 📖	mathematical	—	Set Set.instHasSubset setOf AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership AddSubmonoid.instSetLike AddSubmonoid.closure AddIrreducible	—	AddSubmonoid.closure_induction not_addIrreducible_zero IsEmpty.forall_iff instIsEmptyFalse AddIrreducible.eq_zero_or_eq_zero zero_add add_zero
addIrreducible_subset_of_addSubmonoidClosure_eq_top 📖	mathematical	AddSubmonoid.closure AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Top.top AddSubmonoid AddSubmonoid.instTop	Set Set.instHasSubset setOf AddIrreducible	—	AddSubmonoid.mem_top addIrreducible_mem_addSubmonoidClosure_subset
finite_addIrreducible 📖	mathematical	—	Set.Finite setOf AddIrreducible AddCommMonoid.toAddMonoid	—	AddSubmonoid.mem_top AddSubmonoid.FG.finite_addIrreducible_mem_addSubmonoidClosure AddMonoid.FG.fg_top
finite_irreducible 📖	mathematical	—	Set.Finite setOf Irreducible CommMonoid.toMonoid	—	Submonoid.FG.finite_irreducible_mem_submonoidClosure Monoid.FG.fg_top
irreducible_mem_submonoidClosure_subset 📖	mathematical	—	Set Set.instHasSubset setOf Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike Submonoid.closure Irreducible	—	Submonoid.closure_induction instIsEmptyFalse Irreducible.eq_one_or_eq_one one_mul mul_one
irreducible_subset_of_submonoidClosure_eq_top 📖	mathematical	Submonoid.closure Monoid.toMulOneClass CommMonoid.toMonoid Top.top Submonoid Submonoid.instTop	Set Set.instHasSubset setOf Irreducible	—	irreducible_mem_submonoidClosure_subset

---

← Back to Index