English
The equivalence relation generated by Rel r equals RingConGen.Rel r.
Русский
Эквивалентное отношение, порождаемое Rel r, равно RingConGen.Rel r.
LaTeX
$$Relation.EqvGen (Rel r) = RingConGen.Rel r$$
Lean4
/-- `EqvGen (RingQuot.Rel r)` is a ring congruence. -/
def ringCon (r : R → R → Prop) : RingCon R
where
r := Relation.EqvGen (Rel r)
iseqv := Relation.EqvGen.is_equivalence _
add' {a b c d} hab
hcd := by
induction hab generalizing c d with
| rel _ _ hab =>
refine (Relation.EqvGen.rel _ _ hab.add_left).trans _ _ _ ?_
induction hcd with
| rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.add_right
| refl => exact Relation.EqvGen.refl _
| symm _ _ _ h => exact h.symm _ _
| trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'
| refl =>
induction hcd with
| rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.add_right
| refl => exact Relation.EqvGen.refl _
| symm _ _ _ h => exact h.symm _ _
| trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'
| symm x y _ hxy => exact (hxy hcd.symm).symm
| trans x y z _ _ h h' => exact (h hcd).trans _ _ _ (h' <| Relation.EqvGen.refl _)
mul' {a b c d} hab
hcd := by
induction hab generalizing c d with
| rel _ _ hab =>
refine (Relation.EqvGen.rel _ _ hab.mul_left).trans _ _ _ ?_
induction hcd with
| rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.mul_right
| refl => exact Relation.EqvGen.refl _
| symm _ _ _ h => exact h.symm _ _
| trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'
| refl =>
induction hcd with
| rel _ _ hcd => exact Relation.EqvGen.rel _ _ hcd.mul_right
| refl => exact Relation.EqvGen.refl _
| symm _ _ _ h => exact h.symm _ _
| trans _ _ _ _ _ h h' => exact h.trans _ _ _ h'
| symm x y _ hxy => exact (hxy hcd.symm).symm
| trans x y z _ _ h h' => exact (h hcd).trans _ _ _ (h' <| Relation.EqvGen.refl _)
