Zulip Chat Archive

Stream: maths

Topic: subalgebra.add_mem

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_submonoid.add_mem _ _ S.1 _ _ _ hx hy

Kenny Lau (Dec 23 2019 at 13:44):

is_add_subgroup.add_mem is unfortunately not a thing

Johan Commelin (Dec 23 2019 at 14:03):

Ooh, right, we even need monoids to get the job done :rolling_on_the_floor_laughing:

Last updated: Dec 20 2023 at 11:08 UTC