Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-18 12:21 428aec90

View on Github →

feat(group_theory/congruence): create file about congruence relations (#1690)

  • add congruence.lean
  • add has_mul
  • add definition of congruence relation
  • minor changes
  • responding to review comments
  • fix docstring mistake in setoid.lean

Estimated changes

added structure add_con
added inductive add_con_gen.rel
added theorem con.Inf_def
added theorem con.Inf_le
added theorem con.Inf_to_setoid
added theorem con.Sup_def
added theorem con.Sup_eq_con_gen
added theorem con.coe_eq
added theorem con.coe_mul
added theorem con.con_gen_eq
added theorem con.con_gen_idem
added theorem con.con_gen_le
added theorem con.con_gen_mono
added theorem con.con_gen_of_con
added theorem con.ext'
added theorem con.ext'_iff
added theorem con.ext
added theorem con.ext_iff
added theorem con.inf_def
added theorem con.inf_iff_and
added theorem con.le_Inf
added theorem con.le_def
added def con.mul_ker
added theorem con.mul_ker_mk_eq
added def con.pi
added theorem con.sup_def
added theorem con.sup_eq_con_gen
added theorem con.to_setoid_inj
added structure con
added inductive con_gen.rel
added def con_gen