Skip to content

Commit

Permalink
docs(TensorProduct/Tower): fix doc string of `AlgebraTensorModule.ass…
Browse files Browse the repository at this point in the history
…oc` (#10051)

Matches variable names in the doc string with the variables used in the type signature of `AlgebraTensorModule.assoc`.
  • Loading branch information
chrisflav committed Jan 27, 2024
1 parent ae8f621 commit c6cc35e
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/LinearAlgebra/TensorProduct/Tower.lean
Original file line number Diff line number Diff line change
Expand Up @@ -341,7 +341,7 @@ variable [Algebra A B] [IsScalarTower A B M]

/-- Heterobasic version of `TensorProduct.assoc`:
Linear equivalence between `(M ⊗[A] N) ⊗[R] P` and `M ⊗[A] (N ⊗[R] P)`.
`B`-linear equivalence between `(M ⊗[A] P) ⊗[R] Q` and `M ⊗[A] (P ⊗[R] Q)`.
Note this is especially useful with `A = R` (where it is a "more linear" version of
`TensorProduct.assoc`), or with `B = A`. -/
Expand Down

0 comments on commit c6cc35e

Please sign in to comment.