Stream: new members
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
Jalex Stark (Jul 22 2020 at 02:24):
Last updated: May 08 2021 at 18:17 UTC