From 87a7311338e721a720a17974ccc30257ef7035eb Mon Sep 17 00:00:00 2001 From: Daniel Horton Date: Fri, 10 Apr 2026 10:22:17 -0400 Subject: [PATCH] typo in docstring for exteriorPower --- Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean b/Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean index 6c310de2da0814..1ebc16ae040f93 100644 --- a/Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean +++ b/Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean @@ -74,7 +74,7 @@ section exteriorPower -- New variables `n` and `M`, to get the correct order of variables in the notation. variable (n : ℕ) (M : Type u2) [AddCommGroup M] [Module R M] -/-- Definition of the `n`th exterior power of an `R`-module `N`. We introduce the notation +/-- Definition of the `n`th exterior power of an `R`-module `M`. We introduce the notation `⋀[R]^n M` for `exteriorPower R n M`. -/ abbrev exteriorPower : Submodule R (ExteriorAlgebra R M) := LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M) ^ n