Skip to content

Commit

Permalink
tweak docstrings
Browse files Browse the repository at this point in the history
  • Loading branch information
eric-wieser committed Jul 18, 2023
1 parent 0c0ba14 commit 8f6a6de
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/geometric_algebra/from_mathlib/category_theory.lean
Original file line number Diff line number Diff line change
Expand Up @@ -84,7 +84,7 @@ def CliffordAlgebra : QuadraticModule.{u} R ⥤ Algebra.{u} R :=
variables {M : Type w} [add_comm_group M] [module R M] (Q : quadratic_form R M)

/--
The category of `clifford_hom`s
The category of pairs of algebras and `clifford_hom`s to those algebras.
https://empg.maths.ed.ac.uk/Activities/Spin/Lecture1.pdf
-/
Expand Down

0 comments on commit 8f6a6de

Please sign in to comment.