Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-03 17:56 00a1022f

View on Github →

chore(logic/relation): rename to permit dot notation (#10105)

Estimated changes

Modified src/category_theory/is_connected.lean

Modified src/category_theory/limits/types.lean

Modified src/data/pfunctor/multivariate/M.lean

Modified src/group_theory/free_group.lean

Modified src/logic/relation.lean

added theorem equivalence.eqv_gen_eq

added theorem equivalence.eqv_gen_iff

added theorem eqv_gen.mono

deleted theorem relation.eqv_gen_eq_of_equivalence

deleted theorem relation.eqv_gen_iff_of_equivalence

deleted theorem relation.eqv_gen_mono

added theorem relation.refl_trans_gen.lift'

added theorem relation.refl_trans_gen.lift

added theorem relation.refl_trans_gen.mono

deleted theorem relation.refl_trans_gen_lift'

deleted theorem relation.refl_trans_gen_lift

deleted theorem relation.refl_trans_gen_mono

added theorem relation.trans_gen.closed

added theorem relation.trans_gen.lift'

added theorem relation.trans_gen.lift

deleted theorem relation.trans_gen.trans_gen_closed

deleted theorem relation.trans_gen.trans_gen_eq_self

deleted theorem relation.trans_gen.trans_gen_idem

deleted theorem relation.trans_gen.trans_gen_lift'

deleted theorem relation.trans_gen.trans_gen_lift

deleted theorem relation.trans_gen.transitive_trans_gen

added theorem relation.trans_gen_eq_self

added theorem relation.trans_gen_idem

added theorem relation.transitive_trans_gen

Modified test/qpf.lean