Mathlib v3 is deprecated. Go to Mathlib v4

Theorem function.embedding.coe_quotient_out

Modification history

2022-08-08 19:01
src/logic/embedding.lean
feat(order/rel_iso): `well_founded (quotient.lift₂ r H) ↔ well_founded r` (#15890)
Added function.embedding.coe_quotient_outView on Github →