Commit 2022-02-07 08:33 b1b09eb3

View on Github →

refactor(data/quot): Make more setoid arguments implicit (#11824) Currently, not all of the quotient API can be used with non-instance setoids. This fixes it by making a few setoid arguments explicit rather than instances.

Estimated changes

Modified src/data/quot.lean

modified theorem quotient.out_equiv_out

modified theorem quotient.out_inj

Modified src/group_theory/schur_zassenhaus.lean