Commit 2024-10-19 06:53 a0521c9b

View on Github →

chore: deprecate Setoid.Rel (#16260)

Estimated changes

modified theorem Setoid.bot_def
modified theorem Setoid.comap_rel
modified theorem Setoid.comm'
modified theorem Setoid.eq_iff_rel_eq
modified theorem Setoid.eq_top_iff
modified theorem Setoid.eqvGen_idem
modified theorem Setoid.eqvGen_le
added theorem Setoid.ext'_iff
deleted theorem Setoid.ext_iff
modified def Setoid.gi
modified theorem Setoid.inf_def
modified theorem Setoid.inf_iff_and
modified theorem Setoid.ker_def
modified theorem Setoid.ker_iff_mem_preimage
modified theorem Setoid.le_def
modified theorem Setoid.refl'
modified theorem Setoid.sInf_def
modified theorem Setoid.sSup_def
modified theorem Setoid.sup_def
modified theorem Setoid.symm'
modified theorem Setoid.top_def
modified theorem Setoid.trans'
modified theorem IndexedPartition.class_of
modified theorem IndexedPartition.some_index
modified theorem Setoid.mem_classes
modified theorem MulAction.orbitRel_apply
modified theorem ConjAct.orbitRel_conjAct
modified theorem DiscreteQuotient.fiber_eq
modified theorem DiscreteQuotient.refl
modified theorem DiscreteQuotient.symm
modified theorem DiscreteQuotient.trans
modified theorem t2Quotient.mk_eq