Skip to content

Commit

Permalink
fix broken reference
Browse files Browse the repository at this point in the history
Reference to a mathlib file which no longer exists has been removed, and replaced by a more user-friendly example of an equivalence relation.
  • Loading branch information
kbuzzard committed Feb 26, 2019
1 parent 3f47739 commit 3737387
Showing 1 changed file with 4 additions and 1 deletion.
5 changes: 4 additions & 1 deletion docs/theories/relations.md
Expand Up @@ -30,4 +30,7 @@ defined in `init/data/quot.lean` . The online document
*Theorem Proving In Lean* has
[quite a good section about setoids and quotients](https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html#quotients)

A nice mathematical example can be found in `linear_algebra/quotient_module`.
A nice mathematical example can be found in `linear_algebra/basic.lean`. The definition of `quotient_rel`
says that `x` and `y` are related iff `x - y` is in a fixed submodule `p`, and then it is proved
(rather succinctly) that this is an equivalence relation, and the structure of a module is put
on the equivalence classes. An example more readable for beginners is [here](https://github.com/kbuzzard/xena/blob/master/Examples/zmod37.lean), where the structure of a ring is put on the quotient space Z/37Z.

0 comments on commit 3737387

Please sign in to comment.