Mathlib v3 is deprecated. Go to Mathlib v4

Theorem quotient.out_inj

Modification history

2022-02-07 08:33
src/data/quot.lean
refactor(data/quot): Make more `setoid` arguments implicit (#11824) …
Modified quotient.out_injView on Github →
2021-10-04 19:37
src/data/quot.lean
feat(set_theory/cardinal,*): assorted lemmas (#9516) …
Added quotient.out_injView on Github →