Documentation

Mathlib.GroupTheory.Congruence.Defs

Congruence relations #

This file defines congruence relations: equivalence relations that preserve a binary operation, which in this case is multiplication or addition. The principal definition is a structure extending a Setoid (an equivalence relation), and the inductive definition of the smallest congruence relation containing a binary relation is also given (see ConGen).

The file also proves basic properties of the quotient of a type by a congruence relation, and the complete lattice of congruence relations on a type. We then establish an order-preserving bijection between the set of congruence relations containing a congruence relation c and the set of congruence relations on the quotient by c.

The second half of the file concerns congruence relations on monoids, in which case the quotient by the congruence relation is also a monoid.

Implementation notes #

The inductive definition of a congruence relation could be a nested inductive type, defined using the equivalence closure of a binary relation EqvGen, but the recursor generated does not work. A nested inductive definition could conceivably shorten proofs, because they would allow invocation of the corresponding lemmas about EqvGen.

The lemmas refl, symm and trans are not tagged with @[refl], @[symm], and @[trans] respectively as these tags do not work on a structure coerced to a binary relation.

There is a coercion from elements of a type to the element's equivalence class under a congruence relation.

A congruence relation on a monoid M can be thought of as a submonoid of M × M for which membership is an equivalence relation, but whilst this fact is established in the file, it is not used, since this perspective adds more layers of definitional unfolding.

Tags #

congruence, congruence relation, quotient, quotient by congruence relation, monoid, quotient monoid, isomorphism theorems

structure AddCon (M : Type u_1) [Add M] extends Setoid :
Type u_1

A congruence relation on a type with an addition is an equivalence relation which preserves addition.

  • r : MMProp
  • iseqv : Equivalence self.toSetoid
  • add' : ∀ {w x y z : M}, self.toSetoid w xself.toSetoid y zself.toSetoid (w + y) (x + z)

    Additive congruence relations are closed under addition

Instances For
    theorem AddCon.add' {M : Type u_1} [Add M] (self : AddCon M) {w : M} {x : M} {y : M} {z : M} :
    self.toSetoid w xself.toSetoid y zself.toSetoid (w + y) (x + z)

    Additive congruence relations are closed under addition

    structure Con (M : Type u_1) [Mul M] extends Setoid :
    Type u_1

    A congruence relation on a type with a multiplication is an equivalence relation which preserves multiplication.

    • r : MMProp
    • iseqv : Equivalence self.toSetoid
    • mul' : ∀ {w x y z : M}, self.toSetoid w xself.toSetoid y zself.toSetoid (w * y) (x * z)

      Congruence relations are closed under multiplication

    Instances For
      theorem Con.mul' {M : Type u_1} [Mul M] (self : Con M) {w : M} {x : M} {y : M} {z : M} :
      self.toSetoid w xself.toSetoid y zself.toSetoid (w * y) (x * z)

      Congruence relations are closed under multiplication

      inductive AddConGen.Rel {M : Type u_1} [Add M] (r : MMProp) :
      MMProp

      The inductively defined smallest additive congruence relation containing a given binary relation.

      Instances For
        inductive ConGen.Rel {M : Type u_1} [Mul M] (r : MMProp) :
        MMProp

        The inductively defined smallest multiplicative congruence relation containing a given binary relation.

        Instances For
          def addConGen {M : Type u_1} [Add M] (r : MMProp) :

          The inductively defined smallest additive congruence relation containing a given binary relation.

          Equations
          Instances For
            def conGen {M : Type u_1} [Mul M] (r : MMProp) :
            Con M

            The inductively defined smallest multiplicative congruence relation containing a given binary relation.

            Equations
            Instances For
              instance AddCon.instInhabited {M : Type u_1} [Add M] :
              Equations
              • AddCon.instInhabited = { default := addConGen EmptyRelation }
              instance Con.instInhabited {M : Type u_1} [Mul M] :
              Equations
              • Con.instInhabited = { default := conGen EmptyRelation }
              instance AddCon.instFunLikeForallProp {M : Type u_1} [Add M] :
              FunLike (AddCon M) M (MProp)

              A coercion from an additive congruence relation to its underlying binary relation.

              Equations
              • AddCon.instFunLikeForallProp = { coe := fun (c : AddCon M) => c.toSetoid, coe_injective' := }
              instance Con.instFunLikeForallProp {M : Type u_1} [Mul M] :
              FunLike (Con M) M (MProp)

              A coercion from a congruence relation to its underlying binary relation.

              Equations
              • Con.instFunLikeForallProp = { coe := fun (c : Con M) => c.toSetoid, coe_injective' := }
              @[simp]
              theorem AddCon.rel_eq_coe {M : Type u_1} [Add M] (c : AddCon M) :
              c.toSetoid = c
              @[simp]
              theorem Con.rel_eq_coe {M : Type u_1} [Mul M] (c : Con M) :
              c.toSetoid = c
              theorem AddCon.refl {M : Type u_1} [Add M] (c : AddCon M) (x : M) :
              c x x

              Additive congruence relations are reflexive.

              theorem Con.refl {M : Type u_1} [Mul M] (c : Con M) (x : M) :
              c x x

              Congruence relations are reflexive.

              theorem AddCon.symm {M : Type u_1} [Add M] (c : AddCon M) {x : M} {y : M} :
              c x yc y x

              Additive congruence relations are symmetric.

              theorem Con.symm {M : Type u_1} [Mul M] (c : Con M) {x : M} {y : M} :
              c x yc y x

              Congruence relations are symmetric.

              theorem AddCon.trans {M : Type u_1} [Add M] (c : AddCon M) {x : M} {y : M} {z : M} :
              c x yc y zc x z

              Additive congruence relations are transitive.

              theorem Con.trans {M : Type u_1} [Mul M] (c : Con M) {x : M} {y : M} {z : M} :
              c x yc y zc x z

              Congruence relations are transitive.

              theorem AddCon.add {M : Type u_1} [Add M] (c : AddCon M) {w : M} {x : M} {y : M} {z : M} :
              c w xc y zc (w + y) (x + z)

              Additive congruence relations preserve addition.

              theorem Con.mul {M : Type u_1} [Mul M] (c : Con M) {w : M} {x : M} {y : M} {z : M} :
              c w xc y zc (w * y) (x * z)

              Multiplicative congruence relations preserve multiplication.

              @[simp]
              theorem AddCon.rel_mk {M : Type u_1} [Add M] {s : Setoid M} {h : ∀ {w x y z : M}, s w xs y zs (w + y) (x + z)} {a : M} {b : M} :
              { toSetoid := s, add' := h } a b s a b
              @[simp]
              theorem Con.rel_mk {M : Type u_1} [Mul M] {s : Setoid M} {h : ∀ {w x y z : M}, s w xs y zs (w * y) (x * z)} {a : M} {b : M} :
              { toSetoid := s, mul' := h } a b s a b
              instance AddCon.instMembershipSum {M : Type u_1} [Add M] :
              Membership (M × M) (AddCon M)

              Given a type M with an addition, x, y ∈ M, and an additive congruence relation c on M, (x, y) ∈ M × M iff x is related to y by c.

              Equations
              • AddCon.instMembershipSum = { mem := fun (c : AddCon M) (x : M × M) => c x.1 x.2 }
              instance Con.instMembershipProd {M : Type u_1} [Mul M] :
              Membership (M × M) (Con M)

              Given a type M with a multiplication, a congruence relation c on M, and elements of M x, y, (x, y) ∈ M × M iff x is related to y by c.

              Equations
              • Con.instMembershipProd = { mem := fun (c : Con M) (x : M × M) => c x.1 x.2 }
              theorem AddCon.ext' {M : Type u_1} [Add M] {c : AddCon M} {d : AddCon M} (H : c = d) :
              c = d

              The map sending an additive congruence relation to its underlying binary relation is injective.

              theorem Con.ext' {M : Type u_1} [Mul M] {c : Con M} {d : Con M} (H : c = d) :
              c = d

              The map sending a congruence relation to its underlying binary relation is injective.

              theorem AddCon.ext {M : Type u_1} [Add M] {c : AddCon M} {d : AddCon M} (H : ∀ (x y : M), c x y d x y) :
              c = d

              Extensionality rule for additive congruence relations.

              theorem Con.ext_iff {M : Type u_1} [Mul M] {c : Con M} {d : Con M} :
              c = d ∀ (x y : M), c x y d x y
              theorem AddCon.ext_iff {M : Type u_1} [Add M] {c : AddCon M} {d : AddCon M} :
              c = d ∀ (x y : M), c x y d x y
              theorem Con.ext {M : Type u_1} [Mul M] {c : Con M} {d : Con M} (H : ∀ (x y : M), c x y d x y) :
              c = d

              Extensionality rule for congruence relations.

              theorem AddCon.toSetoid_inj {M : Type u_1} [Add M] {c : AddCon M} {d : AddCon M} (H : c.toSetoid = d.toSetoid) :
              c = d

              The map sending an additive congruence relation to its underlying equivalence relation is injective.

              theorem Con.toSetoid_inj {M : Type u_1} [Mul M] {c : Con M} {d : Con M} (H : c.toSetoid = d.toSetoid) :
              c = d

              The map sending a congruence relation to its underlying equivalence relation is injective.

              theorem AddCon.coe_inj {M : Type u_1} [Add M] {c : AddCon M} {d : AddCon M} :
              c = d c = d

              Two additive congruence relations are equal iff their underlying binary relations are equal.

              theorem Con.coe_inj {M : Type u_1} [Mul M] {c : Con M} {d : Con M} :
              c = d c = d

              Two congruence relations are equal iff their underlying binary relations are equal.

              def AddCon.addKer {M : Type u_1} {P : Type u_3} [Add M] [Add P] (f : MP) (h : ∀ (x y : M), f (x + y) = f x + f y) :

              The kernel of an addition-preserving function as an additive congruence relation.

              Equations
              Instances For
                def Con.mulKer {M : Type u_1} {P : Type u_3} [Mul M] [Mul P] (f : MP) (h : ∀ (x y : M), f (x * y) = f x * f y) :
                Con M

                The kernel of a multiplication-preserving function as a congruence relation.

                Equations
                Instances For
                  def AddCon.Quotient {M : Type u_1} [Add M] (c : AddCon M) :
                  Type u_1

                  Defining the quotient by an additive congruence relation of a type with an addition.

                  Equations
                  Instances For
                    def Con.Quotient {M : Type u_1} [Mul M] (c : Con M) :
                    Type u_1

                    Defining the quotient by a congruence relation of a type with a multiplication.

                    Equations
                    Instances For
                      def AddCon.toQuotient {M : Type u_1} [Add M] {c : AddCon M} :
                      Mc.Quotient

                      The morphism into the quotient by an additive congruence relation

                      Equations
                      • AddCon.toQuotient = Quotient.mk''
                      Instances For
                        def Con.toQuotient {M : Type u_1} [Mul M] {c : Con M} :
                        Mc.Quotient

                        The morphism into the quotient by a congruence relation

                        Equations
                        • Con.toQuotient = Quotient.mk''
                        Instances For
                          @[instance 10]
                          instance AddCon.instCoeTCQuotient {M : Type u_1} [Add M] (c : AddCon M) :
                          CoeTC M c.Quotient

                          Coercion from a type with an addition to its quotient by an additive congruence relation

                          Equations
                          • c.instCoeTCQuotient = { coe := AddCon.toQuotient }
                          @[instance 10]
                          instance Con.instCoeTCQuotient {M : Type u_1} [Mul M] (c : Con M) :
                          CoeTC M c.Quotient

                          Coercion from a type with a multiplication to its quotient by a congruence relation.

                          See Note [use has_coe_t].

                          Equations
                          • c.instCoeTCQuotient = { coe := Con.toQuotient }
                          @[instance 500]
                          instance AddCon.instDecidableEqQuotientOfDecidableCoeForallProp {M : Type u_1} [Add M] (c : AddCon M) [(a b : M) → Decidable (c a b)] :
                          DecidableEq c.Quotient

                          The quotient by a decidable additive congruence relation has decidable equality.

                          Equations
                          @[instance 500]
                          instance Con.instDecidableEqQuotientOfDecidableCoeForallProp {M : Type u_1} [Mul M] (c : Con M) [(a b : M) → Decidable (c a b)] :
                          DecidableEq c.Quotient

                          The quotient by a decidable congruence relation has decidable equality.

                          Equations
                          @[simp]
                          theorem AddCon.quot_mk_eq_coe {M : Type u_4} [Add M] (c : AddCon M) (x : M) :
                          Quot.mk (⇑c) x = x
                          @[simp]
                          theorem Con.quot_mk_eq_coe {M : Type u_4} [Mul M] (c : Con M) (x : M) :
                          Quot.mk (⇑c) x = x
                          def AddCon.liftOn {M : Type u_1} [Add M] {β : Sort u_4} {c : AddCon M} (q : c.Quotient) (f : Mβ) (h : ∀ (a b : M), c a bf a = f b) :
                          β

                          The function on the quotient by a congruence relation c induced by a function that is constant on c's equivalence classes.

                          Equations
                          Instances For
                            def Con.liftOn {M : Type u_1} [Mul M] {β : Sort u_4} {c : Con M} (q : c.Quotient) (f : Mβ) (h : ∀ (a b : M), c a bf a = f b) :
                            β

                            The function on the quotient by a congruence relation c induced by a function that is constant on c's equivalence classes.

                            Equations
                            Instances For
                              def AddCon.liftOn₂ {M : Type u_1} [Add M] {β : Sort u_4} {c : AddCon M} (q : c.Quotient) (r : c.Quotient) (f : MMβ) (h : ∀ (a₁ a₂ b₁ b₂ : M), c a₁ b₁c a₂ b₂f a₁ a₂ = f b₁ b₂) :
                              β

                              The binary function on the quotient by a congruence relation c induced by a binary function that is constant on c's equivalence classes.

                              Equations
                              Instances For
                                def Con.liftOn₂ {M : Type u_1} [Mul M] {β : Sort u_4} {c : Con M} (q : c.Quotient) (r : c.Quotient) (f : MMβ) (h : ∀ (a₁ a₂ b₁ b₂ : M), c a₁ b₁c a₂ b₂f a₁ a₂ = f b₁ b₂) :
                                β

                                The binary function on the quotient by a congruence relation c induced by a binary function that is constant on c's equivalence classes.

                                Equations
                                Instances For
                                  def AddCon.hrecOn₂ {M : Type u_1} {N : Type u_2} [Add M] [Add N] {cM : AddCon M} {cN : AddCon N} {φ : cM.QuotientcN.QuotientSort u_4} (a : cM.Quotient) (b : cN.Quotient) (f : (x : M) → (y : N) → φ x y) (h : ∀ (x : M) (y : N) (x' : M) (y' : N), cM x x'cN y y'HEq (f x y) (f x' y')) :
                                  φ a b

                                  A version of Quotient.hrecOn₂' for quotients by AddCon.

                                  Equations
                                  Instances For
                                    def Con.hrecOn₂ {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {cM : Con M} {cN : Con N} {φ : cM.QuotientcN.QuotientSort u_4} (a : cM.Quotient) (b : cN.Quotient) (f : (x : M) → (y : N) → φ x y) (h : ∀ (x : M) (y : N) (x' : M) (y' : N), cM x x'cN y y'HEq (f x y) (f x' y')) :
                                    φ a b

                                    A version of Quotient.hrecOn₂' for quotients by Con.

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem AddCon.hrec_on₂_coe {M : Type u_1} {N : Type u_2} [Add M] [Add N] {cM : AddCon M} {cN : AddCon N} {φ : cM.QuotientcN.QuotientSort u_4} (a : M) (b : N) (f : (x : M) → (y : N) → φ x y) (h : ∀ (x : M) (y : N) (x' : M) (y' : N), cM x x'cN y y'HEq (f x y) (f x' y')) :
                                      AddCon.hrecOn₂ (↑a) (↑b) f h = f a b
                                      @[simp]
                                      theorem Con.hrec_on₂_coe {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {cM : Con M} {cN : Con N} {φ : cM.QuotientcN.QuotientSort u_4} (a : M) (b : N) (f : (x : M) → (y : N) → φ x y) (h : ∀ (x : M) (y : N) (x' : M) (y' : N), cM x x'cN y y'HEq (f x y) (f x' y')) :
                                      Con.hrecOn₂ (↑a) (↑b) f h = f a b
                                      theorem AddCon.induction_on {M : Type u_1} [Add M] {c : AddCon M} {C : c.QuotientProp} (q : c.Quotient) (H : ∀ (x : M), C x) :
                                      C q

                                      The inductive principle used to prove propositions about the elements of a quotient by an additive congruence relation.

                                      theorem Con.induction_on {M : Type u_1} [Mul M] {c : Con M} {C : c.QuotientProp} (q : c.Quotient) (H : ∀ (x : M), C x) :
                                      C q

                                      The inductive principle used to prove propositions about the elements of a quotient by a congruence relation.

                                      theorem AddCon.induction_on₂ {M : Type u_1} {N : Type u_2} [Add M] [Add N] {c : AddCon M} {d : AddCon N} {C : c.Quotientd.QuotientProp} (p : c.Quotient) (q : d.Quotient) (H : ∀ (x : M) (y : N), C x y) :
                                      C p q

                                      A version of AddCon.induction_on for predicates which take two arguments.

                                      theorem Con.induction_on₂ {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {c : Con M} {d : Con N} {C : c.Quotientd.QuotientProp} (p : c.Quotient) (q : d.Quotient) (H : ∀ (x : M) (y : N), C x y) :
                                      C p q

                                      A version of Con.induction_on for predicates which take two arguments.

                                      @[simp]
                                      theorem AddCon.eq {M : Type u_1} [Add M] (c : AddCon M) {a : M} {b : M} :
                                      a = b c a b

                                      Two elements are related by an additive congruence relation c iff they are represented by the same element of the quotient by c.

                                      @[simp]
                                      theorem Con.eq {M : Type u_1} [Mul M] (c : Con M) {a : M} {b : M} :
                                      a = b c a b

                                      Two elements are related by a congruence relation c iff they are represented by the same element of the quotient by c.

                                      instance AddCon.hasAdd {M : Type u_1} [Add M] (c : AddCon M) :
                                      Add c.Quotient

                                      The addition induced on the quotient by an additive congruence relation on a type with an addition.

                                      Equations
                                      instance Con.hasMul {M : Type u_1} [Mul M] (c : Con M) :
                                      Mul c.Quotient

                                      The multiplication induced on the quotient by a congruence relation on a type with a multiplication.

                                      Equations
                                      @[simp]
                                      theorem AddCon.add_ker_mk_eq {M : Type u_1} [Add M] (c : AddCon M) :
                                      AddCon.addKer AddCon.toQuotient = c

                                      The kernel of the quotient map induced by an additive congruence relation c equals c.

                                      @[simp]
                                      theorem Con.mul_ker_mk_eq {M : Type u_1} [Mul M] (c : Con M) :
                                      Con.mulKer Con.toQuotient = c

                                      The kernel of the quotient map induced by a congruence relation c equals c.

                                      @[simp]
                                      theorem AddCon.coe_add {M : Type u_1} [Add M] {c : AddCon M} (x : M) (y : M) :
                                      (x + y) = x + y

                                      The coercion to the quotient of an additive congruence relation commutes with addition (by definition).

                                      @[simp]
                                      theorem Con.coe_mul {M : Type u_1} [Mul M] {c : Con M} (x : M) (y : M) :
                                      (x * y) = x * y

                                      The coercion to the quotient of a congruence relation commutes with multiplication (by definition).

                                      @[simp]
                                      theorem AddCon.liftOn_coe {M : Type u_1} [Add M] {β : Sort u_4} (c : AddCon M) (f : Mβ) (h : ∀ (a b : M), c a bf a = f b) (x : M) :
                                      AddCon.liftOn (↑x) f h = f x

                                      Definition of the function on the quotient by an additive congruence relation c induced by a function that is constant on c's equivalence classes.

                                      @[simp]
                                      theorem Con.liftOn_coe {M : Type u_1} [Mul M] {β : Sort u_4} (c : Con M) (f : Mβ) (h : ∀ (a b : M), c a bf a = f b) (x : M) :
                                      Con.liftOn (↑x) f h = f x

                                      Definition of the function on the quotient by a congruence relation c induced by a function that is constant on c's equivalence classes.

                                      instance AddCon.instLE {M : Type u_1} [Add M] :

                                      For additive congruence relations c, d on a type M with an addition, c ≤ d iff ∀ x y ∈ M, x is related to y by d if x is related to y by c.

                                      Equations
                                      • AddCon.instLE = { le := fun (c d : AddCon M) => ∀ ⦃x y : M⦄, c x yd x y }
                                      instance Con.instLE {M : Type u_1} [Mul M] :
                                      LE (Con M)

                                      For congruence relations c, d on a type M with a multiplication, c ≤ d iff ∀ x y ∈ M, x is related to y by d if x is related to y by c.

                                      Equations
                                      • Con.instLE = { le := fun (c d : Con M) => ∀ ⦃x y : M⦄, c x yd x y }
                                      theorem AddCon.le_def {M : Type u_1} [Add M] {c : AddCon M} {d : AddCon M} :
                                      c d ∀ {x y : M}, c x yd x y

                                      Definition of for additive congruence relations.

                                      theorem Con.le_def {M : Type u_1} [Mul M] {c : Con M} {d : Con M} :
                                      c d ∀ {x y : M}, c x yd x y

                                      Definition of for congruence relations.

                                      instance AddCon.instInfSet {M : Type u_1} [Add M] :

                                      The infimum of a set of additive congruence relations on a given type with an addition.

                                      Equations
                                      • AddCon.instInfSet = { sInf := fun (S : Set (AddCon M)) => { r := fun (x y : M) => cS, c x y, iseqv := , add' := } }
                                      instance Con.instInfSet {M : Type u_1} [Mul M] :

                                      The infimum of a set of congruence relations on a given type with a multiplication.

                                      Equations
                                      • Con.instInfSet = { sInf := fun (S : Set (Con M)) => { r := fun (x y : M) => cS, c x y, iseqv := , mul' := } }
                                      theorem AddCon.sInf_toSetoid {M : Type u_1} [Add M] (S : Set (AddCon M)) :
                                      (sInf S).toSetoid = sInf (AddCon.toSetoid '' S)

                                      The infimum of a set of additive congruence relations is the same as the infimum of the set's image under the map to the underlying equivalence relation.

                                      theorem Con.sInf_toSetoid {M : Type u_1} [Mul M] (S : Set (Con M)) :
                                      (sInf S).toSetoid = sInf (Con.toSetoid '' S)

                                      The infimum of a set of congruence relations is the same as the infimum of the set's image under the map to the underlying equivalence relation.

                                      @[simp]
                                      theorem AddCon.coe_sInf {M : Type u_1} [Add M] (S : Set (AddCon M)) :
                                      (sInf S) = sInf (DFunLike.coe '' S)

                                      The infimum of a set of additive congruence relations is the same as the infimum of the set's image under the map to the underlying binary relation.

                                      @[simp]
                                      theorem Con.coe_sInf {M : Type u_1} [Mul M] (S : Set (Con M)) :
                                      (sInf S) = sInf (DFunLike.coe '' S)

                                      The infimum of a set of congruence relations is the same as the infimum of the set's image under the map to the underlying binary relation.

                                      @[simp]
                                      theorem AddCon.coe_iInf {M : Type u_1} [Add M] {ι : Sort u_4} (f : ιAddCon M) :
                                      (iInf f) = ⨅ (i : ι), (f i)
                                      @[simp]
                                      theorem Con.coe_iInf {M : Type u_1} [Mul M] {ι : Sort u_4} (f : ιCon M) :
                                      (iInf f) = ⨅ (i : ι), (f i)
                                      instance AddCon.instPartialOrder {M : Type u_1} [Add M] :
                                      Equations
                                      instance Con.instPartialOrder {M : Type u_1} [Mul M] :
                                      Equations

                                      The complete lattice of additive congruence relations on a given type with an addition.

                                      Equations
                                      instance Con.instCompleteLattice {M : Type u_1} [Mul M] :

                                      The complete lattice of congruence relations on a given type with a multiplication.

                                      Equations
                                      @[simp]
                                      theorem AddCon.coe_inf {M : Type u_1} [Add M] {c : AddCon M} {d : AddCon M} :
                                      (c d) = c d

                                      The infimum of two additive congruence relations equals the infimum of the underlying binary operations.

                                      @[simp]
                                      theorem Con.coe_inf {M : Type u_1} [Mul M] {c : Con M} {d : Con M} :
                                      (c d) = c d

                                      The infimum of two congruence relations equals the infimum of the underlying binary operations.

                                      theorem AddCon.inf_iff_and {M : Type u_1} [Add M] {c : AddCon M} {d : AddCon M} {x : M} {y : M} :
                                      (c d) x y c x y d x y

                                      Definition of the infimum of two additive congruence relations.

                                      theorem Con.inf_iff_and {M : Type u_1} [Mul M] {c : Con M} {d : Con M} {x : M} {y : M} :
                                      (c d) x y c x y d x y

                                      Definition of the infimum of two congruence relations.

                                      theorem AddCon.addConGen_eq {M : Type u_1} [Add M] (r : MMProp) :
                                      addConGen r = sInf {s : AddCon M | ∀ (x y : M), r x ys x y}

                                      The inductively defined smallest additive congruence relation containing a binary relation r equals the infimum of the set of additive congruence relations containing r.

                                      theorem Con.conGen_eq {M : Type u_1} [Mul M] (r : MMProp) :
                                      conGen r = sInf {s : Con M | ∀ (x y : M), r x ys x y}

                                      The inductively defined smallest congruence relation containing a binary relation r equals the infimum of the set of congruence relations containing r.

                                      theorem AddCon.addConGen_le {M : Type u_1} [Add M] {r : MMProp} {c : AddCon M} (h : ∀ (x y : M), r x yc x y) :

                                      The smallest additive congruence relation containing a binary relation r is contained in any additive congruence relation containing r.

                                      theorem Con.conGen_le {M : Type u_1} [Mul M] {r : MMProp} {c : Con M} (h : ∀ (x y : M), r x yc x y) :

                                      The smallest congruence relation containing a binary relation r is contained in any congruence relation containing r.

                                      theorem AddCon.addConGen_mono {M : Type u_1} [Add M] {r : MMProp} {s : MMProp} (h : ∀ (x y : M), r x ys x y) :

                                      Given binary relations r, s with r contained in s, the smallest additive congruence relation containing s contains the smallest additive congruence relation containing r.

                                      theorem Con.conGen_mono {M : Type u_1} [Mul M] {r : MMProp} {s : MMProp} (h : ∀ (x y : M), r x ys x y) :

                                      Given binary relations r, s with r contained in s, the smallest congruence relation containing s contains the smallest congruence relation containing r.

                                      @[simp]
                                      theorem AddCon.addConGen_of_addCon {M : Type u_1} [Add M] (c : AddCon M) :
                                      addConGen c = c

                                      Additive congruence relations equal the smallest additive congruence relation in which they are contained.

                                      @[simp]
                                      theorem Con.conGen_of_con {M : Type u_1} [Mul M] (c : Con M) :
                                      conGen c = c

                                      Congruence relations equal the smallest congruence relation in which they are contained.

                                      theorem AddCon.addConGen_idem {M : Type u_1} [Add M] (r : MMProp) :

                                      The map sending a binary relation to the smallest additive congruence relation in which it is contained is idempotent.

                                      theorem Con.conGen_idem {M : Type u_1} [Mul M] (r : MMProp) :

                                      The map sending a binary relation to the smallest congruence relation in which it is contained is idempotent.

                                      theorem AddCon.sup_eq_addConGen {M : Type u_1} [Add M] (c : AddCon M) (d : AddCon M) :
                                      c d = addConGen fun (x y : M) => c x y d x y

                                      The supremum of additive congruence relations c, d equals the smallest additive congruence relation containing the binary relation 'x is related to y by c or d'.

                                      theorem Con.sup_eq_conGen {M : Type u_1} [Mul M] (c : Con M) (d : Con M) :
                                      c d = conGen fun (x y : M) => c x y d x y

                                      The supremum of congruence relations c, d equals the smallest congruence relation containing the binary relation 'x is related to y by c or d'.

                                      theorem AddCon.sup_def {M : Type u_1} [Add M] {c : AddCon M} {d : AddCon M} :
                                      c d = addConGen (c d)

                                      The supremum of two additive congruence relations equals the smallest additive congruence relation containing the supremum of the underlying binary operations.

                                      theorem Con.sup_def {M : Type u_1} [Mul M] {c : Con M} {d : Con M} :
                                      c d = conGen (c d)

                                      The supremum of two congruence relations equals the smallest congruence relation containing the supremum of the underlying binary operations.

                                      theorem AddCon.sSup_eq_addConGen {M : Type u_1} [Add M] (S : Set (AddCon M)) :
                                      sSup S = addConGen fun (x y : M) => cS, c x y

                                      The supremum of a set of additive congruence relations S equals the smallest additive congruence relation containing the binary relation 'there exists c ∈ S such that x is related to y by c'.

                                      theorem Con.sSup_eq_conGen {M : Type u_1} [Mul M] (S : Set (Con M)) :
                                      sSup S = conGen fun (x y : M) => cS, c x y

                                      The supremum of a set of congruence relations S equals the smallest congruence relation containing the binary relation 'there exists c ∈ S such that x is related to y by c'.

                                      theorem AddCon.sSup_def {M : Type u_1} [Add M] {S : Set (AddCon M)} :
                                      sSup S = addConGen (sSup (DFunLike.coe '' S))

                                      The supremum of a set of additive congruence relations is the same as the smallest additive congruence relation containing the supremum of the set's image under the map to the underlying binary relation.

                                      theorem Con.sSup_def {M : Type u_1} [Mul M] {S : Set (Con M)} :
                                      sSup S = conGen (sSup (DFunLike.coe '' S))

                                      The supremum of a set of congruence relations is the same as the smallest congruence relation containing the supremum of the set's image under the map to the underlying binary relation.

                                      def AddCon.gi (M : Type u_1) [Add M] :
                                      GaloisInsertion addConGen DFunLike.coe

                                      There is a Galois insertion of additive congruence relations on a type with an addition M into binary relations on M.

                                      Equations
                                      Instances For
                                        def Con.gi (M : Type u_1) [Mul M] :
                                        GaloisInsertion conGen DFunLike.coe

                                        There is a Galois insertion of congruence relations on a type with a multiplication M into binary relations on M.

                                        Equations
                                        • Con.gi M = { choice := fun (r : MMProp) (x : (conGen r) r) => conGen r, gc := , le_l_u := , choice_eq := }
                                        Instances For
                                          def AddCon.mapGen {M : Type u_1} {N : Type u_2} [Add M] [Add N] (c : AddCon M) (f : MN) :

                                          Given a function f, the smallest additive congruence relation containing the binary relation on f's image defined by 'x ≈ y iff the elements of f⁻¹(x) are related to the elements of f⁻¹(y) by an additive congruence relation c.'

                                          Equations
                                          • c.mapGen f = addConGen fun (x y : N) => ∃ (a : M) (b : M), f a = x f b = y c a b
                                          Instances For
                                            def Con.mapGen {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (c : Con M) (f : MN) :
                                            Con N

                                            Given a function f, the smallest congruence relation containing the binary relation on f's image defined by 'x ≈ y iff the elements of f⁻¹(x) are related to the elements of f⁻¹(y) by a congruence relation c.'

                                            Equations
                                            • c.mapGen f = conGen fun (x y : N) => ∃ (a : M) (b : M), f a = x f b = y c a b
                                            Instances For
                                              def AddCon.mapOfSurjective {M : Type u_1} {N : Type u_2} [Add M] [Add N] (c : AddCon M) (f : MN) (H : ∀ (x y : M), f (x + y) = f x + f y) (h : AddCon.addKer f H c) (hf : Function.Surjective f) :

                                              Given a surjective addition-preserving function f whose kernel is contained in an additive congruence relation c, the additive congruence relation on f's codomain defined by 'x ≈ y iff the elements of f⁻¹(x) are related to the elements of f⁻¹(y) by c.'

                                              Equations
                                              • c.mapOfSurjective f H h hf = { toSetoid := c.mapOfSurjective f h hf, add' := }
                                              Instances For
                                                def Con.mapOfSurjective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (c : Con M) (f : MN) (H : ∀ (x y : M), f (x * y) = f x * f y) (h : Con.mulKer f H c) (hf : Function.Surjective f) :
                                                Con N

                                                Given a surjective multiplicative-preserving function f whose kernel is contained in a congruence relation c, the congruence relation on f's codomain defined by 'x ≈ y iff the elements of f⁻¹(x) are related to the elements of f⁻¹(y) by c.'

                                                Equations
                                                • c.mapOfSurjective f H h hf = { toSetoid := c.mapOfSurjective f h hf, mul' := }
                                                Instances For
                                                  theorem AddCon.mapOfSurjective_eq_mapGen {M : Type u_1} {N : Type u_2} [Add M] [Add N] {c : AddCon M} {f : MN} (H : ∀ (x y : M), f (x + y) = f x + f y) (h : AddCon.addKer f H c) (hf : Function.Surjective f) :
                                                  c.mapGen f = c.mapOfSurjective f H h hf

                                                  A specialization of 'the smallest additive congruence relation containing an additive congruence relation c equals c'.

                                                  theorem Con.mapOfSurjective_eq_mapGen {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {c : Con M} {f : MN} (H : ∀ (x y : M), f (x * y) = f x * f y) (h : Con.mulKer f H c) (hf : Function.Surjective f) :
                                                  c.mapGen f = c.mapOfSurjective f H h hf

                                                  A specialization of 'the smallest congruence relation containing a congruence relation c equals c'.

                                                  def AddCon.comap {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : MN) (H : ∀ (x y : M), f (x + y) = f x + f y) (c : AddCon N) :

                                                  Given types with additions M, N and an additive congruence relation c on N, an addition-preserving map f : M → N induces an additive congruence relation on f's domain defined by 'x ≈ y iff f(x) is related to f(y) by c.'

                                                  Equations
                                                  Instances For
                                                    def Con.comap {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : MN) (H : ∀ (x y : M), f (x * y) = f x * f y) (c : Con N) :
                                                    Con M

                                                    Given types with multiplications M, N and a congruence relation c on N, a multiplication-preserving map f : M → N induces a congruence relation on f's domain defined by 'x ≈ y iff f(x) is related to f(y) by c.'

                                                    Equations
                                                    Instances For
                                                      @[simp]
                                                      theorem AddCon.comap_rel {M : Type u_1} {N : Type u_2} [Add M] [Add N] {f : MN} (H : ∀ (x y : M), f (x + y) = f x + f y) {c : AddCon N} {x : M} {y : M} :
                                                      (AddCon.comap f H c) x y c (f x) (f y)
                                                      @[simp]
                                                      theorem Con.comap_rel {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {f : MN} (H : ∀ (x y : M), f (x * y) = f x * f y) {c : Con N} {x : M} {y : M} :
                                                      (Con.comap f H c) x y c (f x) (f y)
                                                      def AddCon.correspondence {M : Type u_1} [Add M] (c : AddCon M) :
                                                      { d : AddCon M // c d } ≃o AddCon c.Quotient

                                                      Given an additive congruence relation c on a type M with an addition, the order-preserving bijection between the set of additive congruence relations containing c and the additive congruence relations on the quotient of M by c.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        def Con.correspondence {M : Type u_1} [Mul M] (c : Con M) :
                                                        { d : Con M // c d } ≃o Con c.Quotient

                                                        Given a congruence relation c on a type M with a multiplication, the order-preserving bijection between the set of congruence relations containing c and the congruence relations on the quotient of M by c.

                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          instance AddCon.addZeroClass {M : Type u_1} [AddZeroClass M] (c : AddCon M) :
                                                          AddZeroClass c.Quotient

                                                          The quotient of an AddMonoid by an additive congruence relation is an AddMonoid.

                                                          Equations
                                                          instance Con.mulOneClass {M : Type u_1} [MulOneClass M] (c : Con M) :
                                                          MulOneClass c.Quotient

                                                          The quotient of a monoid by a congruence relation is a monoid.

                                                          Equations
                                                          @[simp]
                                                          theorem AddCon.coe_zero {M : Type u_1} [AddZeroClass M] {c : AddCon M} :
                                                          0 = 0

                                                          The 0 of the quotient of an AddMonoid by an additive congruence relation is the equivalence class of the AddMonoid's 0.

                                                          @[simp]
                                                          theorem Con.coe_one {M : Type u_1} [MulOneClass M] {c : Con M} :
                                                          1 = 1

                                                          The 1 of the quotient of a monoid by a congruence relation is the equivalence class of the monoid's 1.

                                                          instance AddCon.Quotient.inhabited {M : Type u_1} [AddZeroClass M] {c : AddCon M} :
                                                          Inhabited c.Quotient

                                                          There exists an element of the quotient of an AddMonoid by a congruence relation (namely 0).

                                                          Equations
                                                          • AddCon.Quotient.inhabited = { default := 0 }
                                                          instance Con.Quotient.inhabited {M : Type u_1} [MulOneClass M] {c : Con M} :
                                                          Inhabited c.Quotient

                                                          There exists an element of the quotient of a monoid by a congruence relation (namely 1).

                                                          Equations
                                                          • Con.Quotient.inhabited = { default := 1 }
                                                          theorem AddCon.nsmul {M : Type u_4} [AddMonoid M] (c : AddCon M) (n : ) {w : M} {x : M} :
                                                          c w xc (n w) (n x)

                                                          Additive congruence relations preserve natural scaling.

                                                          theorem Con.pow {M : Type u_4} [Monoid M] (c : Con M) (n : ) {w : M} {x : M} :
                                                          c w xc (w ^ n) (x ^ n)

                                                          Multiplicative congruence relations preserve natural powers.

                                                          instance AddCon.zero {M : Type u_1} [AddZeroClass M] (c : AddCon M) :
                                                          Zero c.Quotient
                                                          Equations
                                                          instance Con.one {M : Type u_1} [MulOneClass M] (c : Con M) :
                                                          One c.Quotient
                                                          Equations
                                                          instance AddCon.Quotient.nsmul {M : Type u_4} [AddMonoid M] (c : AddCon M) :
                                                          SMul c.Quotient
                                                          Equations
                                                          instance Con.instPowQuotientNat {M : Type u_4} [Monoid M] (c : Con M) :
                                                          Pow c.Quotient
                                                          Equations
                                                          • c.instPowQuotientNat = { pow := fun (x : c.Quotient) (n : ) => Quotient.map' (fun (x : M) => x ^ n) x }
                                                          instance AddCon.addSemigroup {M : Type u_4} [AddSemigroup M] (c : AddCon M) :
                                                          AddSemigroup c.Quotient

                                                          The quotient of an AddSemigroup by an additive congruence relation is an AddSemigroup.

                                                          Equations
                                                          instance Con.semigroup {M : Type u_4} [Semigroup M] (c : Con M) :
                                                          Semigroup c.Quotient

                                                          The quotient of a semigroup by a congruence relation is a semigroup.

                                                          Equations
                                                          instance AddCon.addCommSemigroup {M : Type u_4} [AddCommSemigroup M] (c : AddCon M) :
                                                          AddCommSemigroup c.Quotient

                                                          The quotient of an AddCommSemigroup by an additive congruence relation is an AddCommSemigroup.

                                                          Equations
                                                          instance Con.commSemigroup {M : Type u_4} [CommSemigroup M] (c : Con M) :
                                                          CommSemigroup c.Quotient

                                                          The quotient of a commutative semigroup by a congruence relation is a semigroup.

                                                          Equations
                                                          instance AddCon.addMonoid {M : Type u_4} [AddMonoid M] (c : AddCon M) :
                                                          AddMonoid c.Quotient

                                                          The quotient of an AddMonoid by an additive congruence relation is an AddMonoid.

                                                          Equations
                                                          instance Con.monoid {M : Type u_4} [Monoid M] (c : Con M) :
                                                          Monoid c.Quotient

                                                          The quotient of a monoid by a congruence relation is a monoid.

                                                          Equations
                                                          instance AddCon.addCommMonoid {M : Type u_4} [AddCommMonoid M] (c : AddCon M) :
                                                          AddCommMonoid c.Quotient

                                                          The quotient of an AddCommMonoid by an additive congruence relation is an AddCommMonoid.

                                                          Equations
                                                          instance Con.commMonoid {M : Type u_4} [CommMonoid M] (c : Con M) :
                                                          CommMonoid c.Quotient

                                                          The quotient of a CommMonoid by a congruence relation is a CommMonoid.

                                                          Equations
                                                          theorem AddCon.map_of_add_left_rel_zero {M : Type u_1} [AddMonoid M] (c : AddCon M) (f : MM) (hf : ∀ (x : M), c (f x + x) 0) {x : M} {y : M} (h : c x y) :
                                                          c (f x) (f y)

                                                          Sometimes, an additive group is defined as a quotient of a monoid by an additive congruence relation. Usually, the inverse operation is defined as Setoid.map f _ for some f. This lemma allows to avoid code duplication in the definition of the inverse operation: instead of proving both ∀ x y, c x y → c (f x) (f y) (to define the operation) and ∀ x, c (f x + x) 0 (to prove the group laws), one can only prove the latter.

                                                          theorem Con.map_of_mul_left_rel_one {M : Type u_1} [Monoid M] (c : Con M) (f : MM) (hf : ∀ (x : M), c (f x * x) 1) {x : M} {y : M} (h : c x y) :
                                                          c (f x) (f y)

                                                          Sometimes, a group is defined as a quotient of a monoid by a congruence relation. Usually, the inverse operation is defined as Setoid.map f _ for some f. This lemma allows to avoid code duplication in the definition of the inverse operation: instead of proving both ∀ x y, c x y → c (f x) (f y) (to define the operation) and ∀ x, c (f x * x) 1 (to prove the group laws), one can only prove the latter.

                                                          theorem AddCon.neg {M : Type u_1} [AddGroup M] (c : AddCon M) {x : M} {y : M} (h : c x y) :
                                                          c (-x) (-y)

                                                          Additive congruence relations preserve negation.

                                                          theorem Con.inv {M : Type u_1} [Group M] (c : Con M) {x : M} {y : M} (h : c x y) :

                                                          Multiplicative congruence relations preserve inversion.

                                                          theorem AddCon.sub {M : Type u_1} [AddGroup M] (c : AddCon M) {w : M} {x : M} {y : M} {z : M} :
                                                          c w xc y zc (w - y) (x - z)

                                                          Additive congruence relations preserve subtraction.

                                                          theorem Con.div {M : Type u_1} [Group M] (c : Con M) {w : M} {x : M} {y : M} {z : M} :
                                                          c w xc y zc (w / y) (x / z)

                                                          Multiplicative congruence relations preserve division.

                                                          theorem AddCon.zsmul {M : Type u_1} [AddGroup M] (c : AddCon M) (n : ) {w : M} {x : M} :
                                                          c w xc (n w) (n x)

                                                          Additive congruence relations preserve integer scaling.

                                                          theorem Con.zpow {M : Type u_1} [Group M] (c : Con M) (n : ) {w : M} {x : M} :
                                                          c w xc (w ^ n) (x ^ n)

                                                          Multiplicative congruence relations preserve integer powers.

                                                          instance AddCon.hasNeg {M : Type u_1} [AddGroup M] (c : AddCon M) :
                                                          Neg c.Quotient

                                                          The negation induced on the quotient by an additive congruence relation on a type with a negation.

                                                          Equations
                                                          instance Con.hasInv {M : Type u_1} [Group M] (c : Con M) :
                                                          Inv c.Quotient

                                                          The inversion induced on the quotient by a congruence relation on a type with an inversion.

                                                          Equations
                                                          instance AddCon.hasSub {M : Type u_1} [AddGroup M] (c : AddCon M) :
                                                          Sub c.Quotient

                                                          The subtraction induced on the quotient by an additive congruence relation on a type with a subtraction.

                                                          Equations
                                                          instance Con.hasDiv {M : Type u_1} [Group M] (c : Con M) :
                                                          Div c.Quotient

                                                          The division induced on the quotient by a congruence relation on a type with a division.

                                                          Equations
                                                          instance AddCon.Quotient.zsmul {M : Type u_4} [AddGroup M] (c : AddCon M) :
                                                          SMul c.Quotient

                                                          The integer scaling induced on the quotient by a congruence relation on a type with a subtraction.

                                                          Equations
                                                          instance Con.zpowinst {M : Type u_1} [Group M] (c : Con M) :
                                                          Pow c.Quotient

                                                          The integer power induced on the quotient by a congruence relation on a type with a division.

                                                          Equations
                                                          • c.zpowinst = { pow := fun (x : c.Quotient) (z : ) => Quotient.map' (fun (x : M) => x ^ z) x }
                                                          instance AddCon.addGroup {M : Type u_1} [AddGroup M] (c : AddCon M) :
                                                          AddGroup c.Quotient

                                                          The quotient of an AddGroup by an additive congruence relation is an AddGroup.

                                                          Equations
                                                          instance Con.group {M : Type u_1} [Group M] (c : Con M) :
                                                          Group c.Quotient

                                                          The quotient of a group by a congruence relation is a group.

                                                          Equations
                                                          def AddCon.liftOnAddUnits {M : Type u_1} {α : Type u_4} [AddMonoid M] {c : AddCon M} (u : AddUnits c.Quotient) (f : (x y : M) → c (x + y) 0c (y + x) 0α) (Hf : ∀ (x y : M) (hxy : c (x + y) 0) (hyx : c (y + x) 0) (x' y' : M) (hxy' : c (x' + y') 0) (hyx' : c (y' + x') 0), c x x'c y y'f x y hxy hyx = f x' y' hxy' hyx') :
                                                          α

                                                          In order to define a function (Con.Quotient c)ˣ → α on the units of Con.Quotient c, where c : Con M is a multiplicative congruence on a monoid, it suffices to define a function f that takes elements x y : M with proofs of c (x * y) 1 and c (y * x) 1, and returns an element of α provided that f x y _ _ = f x' y' _ _ whenever c x x' and c y y'.

                                                          Equations
                                                          Instances For
                                                            def Con.liftOnUnits {M : Type u_1} {α : Type u_4} [Monoid M] {c : Con M} (u : c.Quotientˣ) (f : (x y : M) → c (x * y) 1c (y * x) 1α) (Hf : ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1) (x' y' : M) (hxy' : c (x' * y') 1) (hyx' : c (y' * x') 1), c x x'c y y'f x y hxy hyx = f x' y' hxy' hyx') :
                                                            α

                                                            In order to define a function (Con.Quotient c)ˣ → α on the units of Con.Quotient c, where c : Con M is a multiplicative congruence on a monoid, it suffices to define a function f that takes elements x y : M with proofs of c (x * y) 1 and c (y * x) 1, and returns an element of α provided that f x y _ _ = f x' y' _ _ whenever c x x' and c y y'.

                                                            Equations
                                                            Instances For
                                                              @[simp]
                                                              theorem AddCon.liftOnAddUnits_mk {M : Type u_1} {α : Type u_4} [AddMonoid M] {c : AddCon M} (f : (x y : M) → c (x + y) 0c (y + x) 0α) (Hf : ∀ (x y : M) (hxy : c (x + y) 0) (hyx : c (y + x) 0) (x' y' : M) (hxy' : c (x' + y') 0) (hyx' : c (y' + x') 0), c x x'c y y'f x y hxy hyx = f x' y' hxy' hyx') (x : M) (y : M) (hxy : x + y = 0) (hyx : y + x = 0) :
                                                              AddCon.liftOnAddUnits { val := x, neg := y, val_neg := hxy, neg_val := hyx } f Hf = f x y
                                                              @[simp]
                                                              theorem Con.liftOnUnits_mk {M : Type u_1} {α : Type u_4} [Monoid M] {c : Con M} (f : (x y : M) → c (x * y) 1c (y * x) 1α) (Hf : ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1) (x' y' : M) (hxy' : c (x' * y') 1) (hyx' : c (y' * x') 1), c x x'c y y'f x y hxy hyx = f x' y' hxy' hyx') (x : M) (y : M) (hxy : x * y = 1) (hyx : y * x = 1) :
                                                              Con.liftOnUnits { val := x, inv := y, val_inv := hxy, inv_val := hyx } f Hf = f x y
                                                              theorem AddCon.induction_on_addUnits {M : Type u_1} [AddMonoid M] {c : AddCon M} {p : AddUnits c.QuotientProp} (u : AddUnits c.Quotient) (H : ∀ (x y : M) (hxy : c (x + y) 0) (hyx : c (y + x) 0), p { val := x, neg := y, val_neg := , neg_val := }) :
                                                              p u
                                                              theorem Con.induction_on_units {M : Type u_1} [Monoid M] {c : Con M} {p : c.QuotientˣProp} (u : c.Quotientˣ) (H : ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1), p { val := x, inv := y, val_inv := , inv_val := }) :
                                                              p u