## Stream: maths

#### Chris Hughes (Dec 23 2019 at 13:35):

Is this actually not in the library? library_search fails.

import ring_theory.integral_closure

example {R A : Type} [comm_ring A] [comm_ring R] [algebra R A] (S : subalgebra R A)
{x y : A} (hx : x ∈ S) (hy : y ∈ S) : x + y ∈ S := sorry


#### Johan Commelin (Dec 23 2019 at 13:41):

It's not, because is_addsubgroup.add_mem is supposed to solve it.

#### Johan Commelin (Dec 23 2019 at 13:41):

I think that was the reasoning. @Kenny Lau correct me if I'm wrong

#### Kenny Lau (Dec 23 2019 at 13:43):

import ring_theory.integral_closure

example {R A : Type} [comm_ring A] [comm_ring R] [algebra R A] (S : subalgebra R A)
{x y : A} (hx : x ∈ S) (hy : y ∈ S) : x + y ∈ S :=

is_add_subgroup.add_mem is unfortunately not a thing