Theorems · Theorem · linear algebra

Submodule.pi_mono

∀ {R : Type u} {ι : Type x} [inst : Semiring R] {φ : ι → Type u_1} [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] {p q : (i : ι) → Submodule R (φ i)} {s : Set ι},
  (∀ i ∈ s, p i ≤ q i) → Submodule.pi s p ≤ Submodule.pi s q

Defined in: Mathlib.LinearAlgebra.Pi
Cited by: 0 results in Mathlib
Foundations: Depth 24 from the axioms · uses propext, Quot.sound
Assumes: Semiring AddCommMonoid Module

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
Modulestatement and proof · cited by 20,661
Semiringstatement and proof · cited by 13,802
AddCommMonoidstatement and proof · cited by 12,281
Submodulestatement and proof · cited by 7,192
Submodule.pistatement · cited by 34
Set.pi_monoproof · cited by 8

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.