Stream: Is there code for X?

Eric Wieser (Sep 30 2020 at 16:11):

I seem to be having difficulty stating this lemma:

lemma mem_adjoin_eq {R A : Type*} {x : A} [comm_semiring R] [semiring A] [algebra R A] {s : set A} :
x ∈ algebra.adjoin R s ↔ x ∈ subsemiring.closure (set.range (algebra_map R A) ∪ s)
begin
sorry
end


which gives

maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances')


Does this exist already? Am I missing something obvious to make this statement work?

Kenny Lau (Sep 30 2020 at 16:23):

https://github.com/leanprover-community/mathlib/blob/0bb5e5d94d688bdbde8615d924742315cbe19def/src/ring_theory/algebra.lean#L1093

Kenny Lau (Sep 30 2020 at 16:23):

This is exactly how adjoin is defined

Eric Wieser (Sep 30 2020 at 16:24):

I know it is @Kenny Lau, but I can't work out how to unfold that in a proof

Eric Wieser (Sep 30 2020 at 16:25):

The error was becaused I missed the trailing := ...

Last updated: May 07 2021 at 21:10 UTC