Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-04-10 14:38 f85330a8

View on Github →

feat(group_theory/submonoid): relate monoid closure to list product

Estimated changes

Modified group_theory/submonoid.lean

added theorem is_submonoid.list_prod_mem

modified theorem is_submonoid.pow_mem

added theorem is_submonoid.power_subset

added theorem monoid.exists_list_of_mem_closure