Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-20 20:03 9d031be0

View on Github →

feat(group_theory/congruence): quotients of monoids by congruence relations (#1710)

  • add congruence.lean
  • add has_mul
  • add definition of congruence relation
  • minor changes
  • Tidy up second half of congruence.lean
  • tidying docstrings
  • tidying
  • constructive 3rd isom in setoid used in congruence
  • remove import
  • open namespaces earlier
  • responding to PR comments

Estimated changes

modified def setoid.comap
added theorem setoid.comap_eq
modified def setoid.map
added theorem con.coe_one
added def con.comap
added theorem con.comap_eq
added theorem con.comp_mk'_apply
added theorem con.injective_ker_lift
added def con.ker
added def con.ker_lift
added theorem con.ker_lift_mk
added theorem con.ker_lift_range_eq
added theorem con.ker_rel
added theorem con.le_iff
added def con.lift
added theorem con.lift_apply_mk'
added theorem con.lift_coe
added theorem con.lift_comp_mk'
added theorem con.lift_funext
added theorem con.lift_mk'
added theorem con.lift_range
added theorem con.lift_unique
added def con.map
added theorem con.map_apply
added def con.map_gen
added theorem con.mem_coe
added def con.mk'
added theorem con.mk'_ker
added theorem con.mk'_surjective
added def con.of_submonoid
added theorem con.to_submonoid_inj