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

Stream: Is there code for X?

[Eric Wieser]

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]

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

[Eric Wieser]

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