Skip to content

Commit

Permalink
doc(Algebra/Module/LinearMap/End, LinearAlgebra/Dual): fix typos in d…
Browse files Browse the repository at this point in the history
…ocstrings (#11170)

Fix two typos:
* In `LinearAlgebra/Dual`, the doctring of `TensorProduct.dualDistribInvOfBasis` says "An inverse to `dual_tensor_dual_map` given bases.", but `dual_tensor_dual_map` is now called `TensorProduct.dualDistrib`.
* In `Algebra/Module/LinearMap/End`, the doctstring of `LinearMap.smulRight` says "When `f` is an `R`-linear map taking values in `S`, then `fun ↦ b, f b • x` is an `R`-linear map.". The map should be `fun b ↦ f b • x`.
  • Loading branch information
smorel394 committed Mar 5, 2024
1 parent a49c6bc commit dcaca11
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 2 deletions.
2 changes: 1 addition & 1 deletion Mathlib/Algebra/Module/LinearMap/End.lean
Expand Up @@ -343,7 +343,7 @@ section SMulRight
variable [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁]
variable [Semiring S] [Module R S] [Module S M] [IsScalarTower R S M]

/-- When `f` is an `R`-linear map taking values in `S`, then `fun ↦ b, f b • x` is an `R`-linear
/-- When `f` is an `R`-linear map taking values in `S`, then `fun b ↦ f b • x` is an `R`-linear
map. -/
def smulRight (f : M₁ →ₗ[R] S) (x : M) : M₁ →ₗ[R] M where
toFun b := f b • x
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/LinearAlgebra/Dual.lean
Expand Up @@ -1793,7 +1793,7 @@ variable [CommRing R] [AddCommGroup M] [AddCommGroup N]

variable [Module R M] [Module R N]

/-- An inverse to `dual_tensor_dual_map` given bases.
/-- An inverse to `TensorProduct.dualDistrib` given bases.
-/
noncomputable def dualDistribInvOfBasis (b : Basis ι R M) (c : Basis κ R N) :
Dual R (M ⊗[R] N) →ₗ[R] Dual R M ⊗[R] Dual R N :=
Expand Down

0 comments on commit dcaca11

Please sign in to comment.