Mathlib v3 is deprecated. Go to Mathlib v4

Theorem submonoid.supr_eq_closure

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.supr_eq_closureView on Github →