Zulip Chat Archive

Stream: Is there code for X?

Topic: algebra.adjoin is subring.closure


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

view this post on Zulip Adam Topaz (Sep 30 2020 at 16:12):

What are your imports?

view this post on Zulip Kenny Lau (Sep 30 2020 at 16:23):

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

view this post on Zulip Kenny Lau (Sep 30 2020 at 16:23):

This is exactly how adjoin is defined

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

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