Additive closures in rings

This file gives criteria for the additive closure of a set in a ring to be closed under multiplication, and hence to coincide with the underlying additive subgroup of the subring generated by that set.

Main results

• Ado.AddSubgroup.mul_mem_closure_of_mul_mem: products of elements of an additive closure remain in the closure when this holds for its generators.
• AddSubgroup.closure_mul_closure: the product of two additive closures is the additive closure of the pairwise products.
• Subring.toAddSubgroup_closure_of_one_mem_of_mul_mem: under the corresponding hypotheses, the subring and additive-subgroup closures have the same underlying additive group.

theorem AddSubgroup.closure_mul_closure {R : Type u_1} [NonUnitalNonAssocRing R] (S T : Set R) : closure S * closure T = closure (S * T)

The product of two additive closures is the additive closure of the pairwise products.

This is the additive-subgroup analogue of AddSubmonoid.closure_mul_closure from Mathlib.Algebra.Ring.Submonoid.Pointwise.

theorem Ado.AddSubgroup.mul_mem_closure_of_mul_mem {R : Type u_2} [NonUnitalNonAssocRing R] {s : Set R} (hs : ∀ x ∈ s, ∀ y ∈ s, x * y ∈ AddSubgroup.closure s) {x y : R} (hx : x ∈ AddSubgroup.closure s) (hy : y ∈ AddSubgroup.closure s) : x * y ∈ AddSubgroup.closure s

If products of generators lie in their additive closure, then that additive closure is closed under multiplication.

theorem Subring.toAddSubgroup_closure_of_one_mem_of_mul_mem {R : Type u_2} [NonAssocRing R] {s : Set R} (h1 : 1 ∈ AddSubgroup.closure s) (hmul : ∀ x ∈ s, ∀ y ∈ s, x * y ∈ AddSubgroup.closure s) : (closure s).toAddSubgroup = AddSubgroup.closure s

If the additive closure of a set contains one and products of generators lie in that closure, then it is the underlying additive subgroup of the subring closure of the set.