Mathlib v3 is deprecated. Go to Mathlib v4

Theorem submonoid.closure_singleton_le_iff_mem

Modification history

2022-01-18 17:08
src/group_theory/submonoid/basic.lean
feat(linear_algebra,algebra,group_theory): miscellaneous lemmas linking some additive monoid and module operations (#11525) …
Added submonoid.closure_singleton_le_iff_memView on Github →