Zulip Chat Archive

Stream: maths

Topic: subalgebra.add_mem


view this post on Zulip 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

view this post on Zulip Johan Commelin (Dec 23 2019 at 13:41):

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

view this post on Zulip Johan Commelin (Dec 23 2019 at 13:41):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Dec 23 2019 at 13:44):

is_add_subgroup.add_mem is unfortunately not a thing

view this post on Zulip 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: May 19 2021 at 03:22 UTC