Finite

📁 Source: Mathlib/Algebra/Group/Submonoid/Finite.lean

Statistics

Metric	Count
Definitions	0
Theorems closure_pi, pi_le_iff, pi_mem_of_single_mem, pi_mem_of_single_mem_aux, closure_pi, pi_le_iff, pi_mem_of_mulSingle_mem, pi_mem_of_mulSingle_mem_aux	8
Total	8

AddSubmonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_pi 📖	mathematical	Set Set.instMembership AddZero.toZero AddZeroClass.toAddZero	closure Pi.addZeroClass Set.pi Set.univ pi	—	le_antisymm closure_le Set.pi_subset_pi_iff subset_closure AddMonoidHom.instAddMonoidHomClass pi_le_iff map_le_of_le_comap Set.mem_univ_pi Pi.single_eq_same Pi.single_eq_of_ne
pi_le_iff 📖	mathematical	—	AddSubmonoid Pi.addZeroClass Preorder.toLE PartialOrder.toPreorder instPartialOrder pi Set.univ map AddMonoidHom AddZeroClass.toAddZero AddMonoidHom.instFunLike AddMonoidHom.instAddMonoidHomClass AddMonoidHom.single	—	AddMonoidHom.instAddMonoidHomClass single_mem_pi Set.mem_univ pi_mem_of_single_mem instAddSubmonoidClass mem_map_of_mem
pi_mem_of_single_mem 📖	—	SetLike.instMembership Pi.single AddZero.toZero AddZeroClass.toAddZero	—	—	nonempty_fintype pi_mem_of_single_mem_aux Finset.mem_univ IsEmpty.forall_iff instIsEmptyFalse
pi_mem_of_single_mem_aux 📖	—	AddZero.toZero AddZeroClass.toAddZero SetLike.instMembership Pi.single	—	—	Finset.induction_on Finset.notMem_empty ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass Function.update_self Pi.single_eq_same zero_add Function.update_of_ne Pi.single_eq_of_ne add_zero AddMemClass.add_mem AddSubmonoidClass.toAddMemClass Finset.mem_insert Finset.mem_insert_of_mem

Submonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_pi 📖	mathematical	Set Set.instMembership MulOne.toOne MulOneClass.toMulOne	closure Pi.mulOneClass Set.pi Set.univ pi	—	le_antisymm closure_le Set.pi_subset_pi_iff subset_closure MonoidHom.instMonoidHomClass pi_le_iff map_le_of_le_comap Set.mem_univ_pi Pi.mulSingle_eq_same Pi.mulSingle_eq_of_ne
pi_le_iff 📖	mathematical	—	Submonoid Pi.mulOneClass Preorder.toLE PartialOrder.toPreorder instPartialOrder pi Set.univ map MonoidHom MulOneClass.toMulOne MonoidHom.instFunLike MonoidHom.instMonoidHomClass MonoidHom.mulSingle	—	MonoidHom.instMonoidHomClass pi_mem_of_mulSingle_mem instSubmonoidClass mem_map_of_mem
pi_mem_of_mulSingle_mem 📖	—	SetLike.instMembership Pi.mulSingle MulOne.toOne MulOneClass.toMulOne	—	—	nonempty_fintype pi_mem_of_mulSingle_mem_aux instIsEmptyFalse
pi_mem_of_mulSingle_mem_aux 📖	—	MulOne.toOne MulOneClass.toMulOne SetLike.instMembership Pi.mulSingle	—	—	Finset.induction_on Finset.notMem_empty OneMemClass.one_mem SubmonoidClass.toOneMemClass Function.update_self Pi.mulSingle_eq_same one_mul Function.update_of_ne Pi.mulSingle_eq_of_ne mul_one MulMemClass.mul_mem SubmonoidClass.toMulMemClass Finset.mem_insert_of_mem

---

← Back to Index