Mathlib v3 is deprecated. Go to Mathlib v4

Theorem monoid.is_submonoid_closure

Modification history

2018-04-10 13:58
group_theory/submonoid.lean
refactor(ring_theory): unify monoid closure in ring theory with the one in group theory
Deleted monoid.is_submonoid_closureView on Github →
2018-04-10 13:13
group_theory/submonoid.lean
feat(group_theory): add subtype instanes for group and monoid; monoid closure
Added monoid.is_submonoid_closureView on Github →