Skip to content

Commit d3ddb19

Browse files
committed
chore(LinearAlgebra/Pi): Fix typos in Submodule.pi docstring (leanprover-community#39156)
The docstring referenced `pi I s` (the parameter is named `p` not `s`) and `p a` (the bound variable is `i` not `a`).
1 parent 155823b commit d3ddb19

1 file changed

Lines changed: 2 additions & 2 deletions

File tree

Mathlib/LinearAlgebra/Pi.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -369,8 +369,8 @@ variable [Semiring R] {φ : ι → Type*} [(i : ι) → AddCommMonoid (φ i)] [(
369369
open LinearMap
370370

371371
/-- A version of `Set.pi` for submodules. Given an index set `I` and a family of submodules
372-
`p : (i : ι) → Submodule R (φ i)`, `pi I s` is the submodule of dependent functions
373-
`f : (i : ι) → φ i` such that `f i` belongs to `p a` whenever `i ∈ I`. -/
372+
`p : (i : ι) → Submodule R (φ i)`, `pi I p` is the submodule of dependent functions
373+
`f : (i : ι) → φ i` such that `f i` belongs to `p i` whenever `i ∈ I`. -/
374374
@[simps]
375375
def pi (I : Set ι) (p : (i : ι) → Submodule R (φ i)) : Submodule R ((i : ι) → φ i) where
376376
carrier := Set.pi I fun i => p i

0 commit comments

Comments
 (0)