## Stream: new members

### Topic: mem_subtype

#### Jalex Stark (Jul 22 2020 at 02:23):

if i have an element of a subtype, how do i show its coercion is contained in the set corresponding to that subtype?

import ring_theory.ideals

example (R : Type*) [comm_ring R]
(P : ideal R)  (c : P) :
(c : R) ∈ P :=
begin

oh, it's apply c.property