Mathlib v3 is deprecated. Go to Mathlib v4

Theorem subsemiring.closure_add_submonoid_closure

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