Zulip Chat Archive

Stream: new members

Topic: mem_subtype


view this post on Zulip 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
  admit
end

view this post on Zulip Jalex Stark (Jul 22 2020 at 02:24):

oh, it's apply c.property


Last updated: May 08 2021 at 18:17 UTC