Theorems · Definition · linear algebra

Submodule.pi

{R : Type u} →
  {ι : Type x} →
    [inst : Semiring R] →
      {φ : ι → Type u_1} →
        [inst_1 : (i : ι) → AddCommMonoid (φ i)] →
          [inst_2 : (i : ι) → Module R (φ i)] → Set ι → ((i : ι) → Submodule R (φ i)) → Submodule R ((i : ι) → φ i)

A version of Set.pi for submodules. Given an index set I and a family of submodules p : (i : ι) → Submodule R (φ i), pi I p is the submodule of dependent functions f : (i : ι) → φ i such that f i belongs to p i whenever i ∈ I.

Defined in

Mathlib.LinearAlgebra.Pi

Cited by

34 results in Mathlib

Foundations

Depth 16 from the axioms · uses Quot.sound

Assumes

SemiringAddCommMonoidModule