We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 2a813c4 commit 87a7311Copy full SHA for 87a7311
1 file changed
Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean
@@ -74,7 +74,7 @@ section exteriorPower
74
-- New variables `n` and `M`, to get the correct order of variables in the notation.
75
variable (n : ℕ) (M : Type u2) [AddCommGroup M] [Module R M]
76
77
-/-- 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
78
`⋀[R]^n M` for `exteriorPower R n M`. -/
79
abbrev exteriorPower : Submodule R (ExteriorAlgebra R M) :=
80
LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M) ^ n
0 commit comments