Skip to content

Commit

Permalink
doc: fix typo (#10360)
Browse files Browse the repository at this point in the history
Fixed minor typo.
  • Loading branch information
pitmonticone committed Feb 9, 2024
1 parent 2e153a6 commit c94fc52
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/LinearAlgebra/Alternating/Basic.lean
Expand Up @@ -22,7 +22,7 @@ arguments of the same type.
* `f.map_perm` expresses how `f` varies by a sign change under a permutation of its inputs.
* An `AddCommMonoid`, `AddCommGroup`, and `Module` structure over `AlternatingMap`s that
matches the definitions over `MultilinearMap`s.
* `MultilinearMap.domDomCongr`, for permutating the elements within a family.
* `MultilinearMap.domDomCongr`, for permuting the elements within a family.
* `MultilinearMap.alternatization`, which makes an alternating map out of a non-alternating one.
* `AlternatingMap.curryLeft`, for binding the leftmost argument of an alternating map indexed
by `Fin n.succ`.
Expand Down

0 comments on commit c94fc52

Please sign in to comment.