Mathlib v3 is deprecated. Go to Mathlib v4

Def submonoid.subsemiring_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 submonoid.subsemiring_closureView on Github →