Commit 2021-08-11 15:48 7b5c60db
View on Github →feat(data/equiv/basic): add a small lemma for simplifying map between equivalent quotient spaces induced by equivalent relations (#8617)
Just adding a small lemma that allows us to compute the composition of the map given by quot.congr with quot.mk