mathlib3
87a021cd - feat(data/quot): `quotient.rec_on_subsingleton` with implicit setoid (#6346)

Commit

4 years ago

feat(data/quot): `quotient.rec_on_subsingleton` with implicit setoid (#6346)

Author

b-mehta

b-mehta

Parents

Loading