Zulip Chat Archive

Stream: Is there code for X?

Topic: nat cast is a member of ideal / subring if 1 is


view this post on Zulip Eric Wieser (Jan 19 2021 at 16:06):

Do we have something like this?

lemma ideal.nat_cast_mem {R : Type*} [comm_ring R] (I : ideal R) (h : (1 : R)  I) :
   (x : ), (x : R)  I
| 0 := I.zero_mem
| (n + 1) := I.add_mem (ideal.nat_cast_mem n) h

If not, is this a reasonable name? And is this lemma actually useful?

view this post on Zulip Alex J. Best (Jan 19 2021 at 16:49):

Can't you just rw docs#ideal.eq_top_iff_one and then mem_top?

view this post on Zulip Eric Wieser (Jan 19 2021 at 16:51):

Ah you're right, that statement isn't interesting


Last updated: May 07 2021 at 22:14 UTC