Commit 2023-01-25 20:19 981b0bcb

View on Github →

feat: port Deprecated.Submonoid (#1666)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Deprecated/Submonoid.lean

added inductive AddMonoid.InClosure

added theorem Additive.isAddSubmonoid

added theorem Additive.is_add_submonoid_iff

added structure IsAddSubmonoid

added theorem IsSubmonoid.Inter

added theorem IsSubmonoid.finset_prod_mem

added theorem IsSubmonoid.image

added theorem IsSubmonoid.inter

added theorem IsSubmonoid.list_prod_mem

added theorem IsSubmonoid.multiset_prod_mem

added theorem IsSubmonoid.pow_mem

added theorem IsSubmonoid.power_subset

added theorem IsSubmonoid.preimage

added structure IsSubmonoid

added def Monoid.Closure

added inductive Monoid.InClosure

added theorem Monoid.closure.IsSubmonoid

added theorem Monoid.closure_mono

added theorem Monoid.closure_singleton

added theorem Monoid.closure_subset

added theorem Monoid.exists_list_of_mem_closure

added theorem Monoid.image_closure

added theorem Monoid.mem_closure_union_iff

added theorem Monoid.subset_closure

added theorem Multiplicative.isSubmonoid

added theorem Multiplicative.isSubmonoid_iff

added theorem Range.is_submonoid

added theorem Submonoid.is_submonoid

added def Submonoid.of

added theorem Univ.IsSubmonoid

added theorem is_submonoid_Union_of_directed

added theorem powers.is_submonoid

added theorem powers.mul_mem

added theorem powers.one_mem

added theorem powers.self_mem

added def powers