mem_subtype

Stream: new members

[Jalex Stark]

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
  admit
end

[Jalex Stark]

oh, it's apply c.property