Stream: Is there code for X?

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

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?

Alex J. Best (Jan 19 2021 at 16:49):

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

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