summaryrefslogtreecommitdiff
path: root/library/relation
diff options
context:
space:
mode:
authoradelon <22380201+adelon@users.noreply.github.com>2025-07-08 21:20:20 +0200
committeradelon <22380201+adelon@users.noreply.github.com>2025-07-08 21:20:20 +0200
commit51fe28bdd9943e359de5835d2737c0fdc8618df7 (patch)
treed21664e4d77d38c7ec4a941670b10f5c94071365 /library/relation
parentdb353b6d19eb5cb4181b64fe37a1bd550395169c (diff)
Linting and optimization
Diffstat (limited to 'library/relation')
-rw-r--r--library/relation/equivalence.tex2
1 files changed, 1 insertions, 1 deletions
diff --git a/library/relation/equivalence.tex b/library/relation/equivalence.tex
index 0c5dbfa..f8b1ba7 100644
--- a/library/relation/equivalence.tex
+++ b/library/relation/equivalence.tex
@@ -180,7 +180,7 @@
\begin{proof}
Take $a\in A$ such that $C = \equivalenceClass{E}{a}$.
Then $a\in \equivalenceClass{E}{a}$.
- $C$ is inhabited by \cref{quotient,inhabited,equivclasses_inhabited}.
+ $C$ is inhabited by \cref{quotient,equivclasses_inhabited}.
\end{proof}
\begin{proposition}\label{quotient_elems_type}