baseChange_span — Mathlib

English

Base-change commutes with span: baseChange_A(span_R s) = span_A (TensorProduct.mk R A M 1 '' s).

Русский

BaseChange сохраняет порождение: baseChange_A(span_R s) = span_A (TensorProduct.mk R A M 1 '' s).

LaTeX

$$$$ \\mathrm{baseChange}_A(\\mathrm{span}_R s)=\\mathrm{span}_A\\bigl(\\mathrm{TensorProduct.mk}\\; R\\; A\\; M\\; 1 '' s\\bigr). $$$$

Lean4

@[simp]
theorem baseChange_span (s : Set M) : (span R s).baseChange A = span A (TensorProduct.mk R A M 1 '' s) := by
  rw [baseChange_eq_span, map_span, span_span_of_tower]

Похожие утверждения