algebra.adjoin API

Stream: Is there code for X?

[Kevin Buzzard]

Do we not have these?

import algebra.algebra.subalgebra.basic

example (A B : Type) [comm_ring A] [comm_ring B] [algebra A B] (S : set B) (s : B) (hs : s ∈ S) :
  s ∈ algebra.adjoin A S :=
begin
  sorry
end

example (A B : Type) [comm_ring A] [comm_ring B] [algebra A B] (S : set B) (a : A) :
  algebra_map A B a ∈ algebra.adjoin A S :=
begin
  sorry
end

I was expecting theorems called things like algebra.mem_adjoin_of... but I've failed to find them. Maybe I'm missing an import? You can rewrite algebra.mem_adjoin_iff which reduces the question to subring.closure but I can't find the API for that either :-/

[Alex J. Best]

First is docs#algebra.subset_adjoin I think?

[Kevin Buzzard]

Aah, I'm looking for mem and it's subset!

[Eric Wieser]

Second is docs#subalgebra.algebra_map_mem

[Eric Rodriguez]

Yeah the adjoin api tends to use a lot the subset mem = mem constructions; I'd generally look for subsetresults.