Commit 2022-11-10 23:34 8983526d

View on Github →

feat: port Data.Quot (#559) This is my first PR to mathlib4 so please check carefully! This PR ports data.quot and the definition of eqv_gen from core Lean 3.

Estimated changes

added theorem Quot.eq
added def Quot.factor
added theorem Quot.factor_mk_eq
added theorem Quot.lift_mk
added theorem Quot.lift_on_mk
added theorem Quot.lift_on₂_mk
added theorem Quot.lift₂_mk
added theorem Quot.map₂_mk
added theorem Quot.out_eq
added theorem Quotient.choice_eq
added theorem Quotient.eq
added theorem Quotient.eq_mk_iff_out
added theorem Quotient.exact'
added theorem Quotient.hrec_on'_mk''
added theorem Quotient.lift_comp_mk
added theorem Quotient.lift_mk
added theorem Quotient.lift_on_mk
added theorem Quotient.lift_on₂_mk
added theorem Quotient.lift₂_mk
added theorem Quotient.map'_mk''
added theorem Quotient.map'_mk
added theorem Quotient.map_mk
added theorem Quotient.map₂'_mk''
added theorem Quotient.map₂_mk
added theorem Quotient.mk_eq_iff_out
added theorem Quotient.mk_out'
added theorem Quotient.mk_out
added theorem Quotient.out_eq'
added theorem Quotient.out_eq
added theorem Quotient.out_equiv_out
added theorem Quotient.out_inj
added theorem Quotient.out_injective
added theorem Quotient.sound'
added theorem Setoid.ext
added def Trunc.bind
added theorem Trunc.exists_rep
added theorem Trunc.ind
added def Trunc.lift
added def Trunc.map
added def Trunc.mk
added theorem Trunc.out_eq
added def Trunc.{u}
added theorem forall_quotient_iff
added theorem nonempty_quotient_iff
added theorem surjective_quot_mk
added theorem surjective_quotient_mk
added theorem true_equivalence
added def EqvGen.Setoid
added theorem EqvGen.is_equivalence
added inductive EqvGen
added theorem Quot.EqvGen_sound
added theorem Quot.exact