Commit 2024-10-09 14:28 7299b3f4

View on Github →

chore(Data/Quot): [s : Setoid α] => {s : Setoid α} (#16256)

Estimated changes

modified theorem Quotient.choice_eq
modified theorem Quotient.eq
modified theorem Quotient.eq_mk_iff_out
modified theorem Quotient.induction_on_pi
modified theorem Quotient.liftOn_mk
modified theorem Quotient.liftOn₂_mk
modified theorem Quotient.lift_comp_mk
modified theorem Quotient.lift_mk
modified theorem Quotient.lift₂_mk
modified theorem Quotient.map'_mk
modified theorem Quotient.mk_eq_iff_out
modified theorem Quotient.mk_out
modified theorem Quotient.out_eq
modified theorem Setoid.ker_apply_mk_out