Theorems · Theorem · linear algebra

PiTensorProduct.lifts_smul

∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] {x : PiTensorProduct R fun i => s i} {p : FreeAddMonoid (R × ((i : ι) → s i))},
  p ∈ x.lifts → ∀ (a : R), (FreeAddMonoid.map fun y => (a * y.1, y.2)) p ∈ (a • x).lifts

If an element p of FreeAddMonoid (R × Π i, s i) lifts an element x of ⨂[R] i, s i, and if a is an element of R, then the list obtained by multiplying the first entry of each element of p by a lifts a • x.

Defined in

Mathlib.LinearAlgebra.PiTensorProduct.Basic

Cited by

1 results in Mathlib

Foundations

Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringAddCommMonoidModule