Commit 2023-01-20 12:37 97dade0f

View on Github →

feat: port GroupTheory.Submonoid.Membership (#1699)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/GroupTheory/Submonoid/Basic.lean

Created Mathlib/GroupTheory/Submonoid/Membership.lean

added theorem AddSubmonoid.closure_singleton_eq

added theorem AddSubmonoid.closure_singleton_zero

added theorem AddSubmonoid.mem_closure_singleton

added def AddSubmonoid.multiples

added theorem FreeMonoid.closure_range_of

added theorem FreeMonoid.mrange_lift

added theorem IsScalarTower.of_mclosure_eq_top

added theorem MulMemClass.mul_left_mem_add_closure

added theorem MulMemClass.mul_mem_add_closure

added theorem MulMemClass.mul_right_mem_add_closure

added theorem SMulCommClass.of_mclosure_eq_top

added def Submonoid.closureCommMonoidOfComm

added theorem Submonoid.closure_eq_image_prod

added theorem Submonoid.closure_eq_mrange

added theorem Submonoid.closure_induction_left

added theorem Submonoid.closure_induction_right

added theorem Submonoid.closure_singleton_eq

added theorem Submonoid.closure_singleton_one

added theorem Submonoid.coe_finset_prod

added theorem Submonoid.coe_list_prod

added theorem Submonoid.coe_multiset_prod

added theorem Submonoid.coe_supᵢ_of_directed

added theorem Submonoid.coe_supₛ_of_directedOn

added theorem Submonoid.exists_list_of_mem_closure

added theorem Submonoid.exists_multiset_of_mem_closure

added theorem Submonoid.induction_of_closure_eq_top_left

added theorem Submonoid.induction_of_closure_eq_top_right

added theorem Submonoid.list_prod_mem

added def Submonoid.log

added theorem Submonoid.log_mul

added theorem Submonoid.log_pow_eq_self

added theorem Submonoid.log_pow_int_eq_self

added theorem Submonoid.map_powers

added theorem Submonoid.mem_closure_pair

added theorem Submonoid.mem_closure_singleton

added theorem Submonoid.mem_closure_singleton_self

added theorem Submonoid.mem_powers

added theorem Submonoid.mem_powers_iff

added theorem Submonoid.mem_sup

added theorem Submonoid.mem_sup_left

added theorem Submonoid.mem_sup_right

added theorem Submonoid.mem_supᵢ_of_directed

added theorem Submonoid.mem_supᵢ_of_mem

added theorem Submonoid.mem_supₛ_of_directedOn

added theorem Submonoid.mem_supₛ_of_mem

added theorem Submonoid.mul_mem_sup

added theorem Submonoid.multiset_noncomm_prod_mem

added theorem Submonoid.multiset_prod_mem

added theorem Submonoid.noncomm_prod_mem

added def Submonoid.pow

added def Submonoid.powLogEquiv

added theorem Submonoid.pow_apply

added theorem Submonoid.pow_log_eq_self

added theorem Submonoid.pow_right_injective_iff_pow_injective

added def Submonoid.powers

added theorem Submonoid.powers_eq_closure

added theorem Submonoid.powers_one

added theorem Submonoid.powers_subset

added theorem Submonoid.prod_mem

added theorem Submonoid.sup_eq_range

added theorem Submonoid.supᵢ_induction'

added theorem Submonoid.supᵢ_induction

added theorem SubmonoidClass.coe_finset_prod

added theorem SubmonoidClass.coe_list_prod

added theorem SubmonoidClass.coe_multiset_prod

added theorem list_prod_mem

added theorem multiset_prod_mem

added theorem ofAdd_image_multiples_eq_powers_ofAdd

added theorem ofMul_image_powers_eq_multiples_ofMul

added theorem prod_mem

Modified Mathlib/GroupTheory/Submonoid/Operations.lean

Modified Mathlib/Order/Directed.lean