Mathlib v3 is deprecated. Go to Mathlib v4

Theorem submonoid.subsemiring_closure_to_add_submonoid

Modification history

2021-04-06 18:32
src/ring_theory/subsemiring.lean
feat(algebra/add_submonoid_closure): the additive closure of a multiplicative submonoid is a subsemiring (#6860) …
Added submonoid.subsemiring_closure_to_add_submonoidView on Github →