English
If a linear map f maps each coordinate into I, then the image lies in I as well.
Русский
Если линейное отображение f направляет каждую координату в I, то образ тоже лежит в I.
LaTeX
$$Theorem map_pi$$
Lean4
/-- If `f : R^n → R^m` is an `R`-linear map and `I ⊆ R` is an ideal, then the image of `I^n` is
contained in `I^m`. -/
theorem map_pi [I.IsTwoSided] {ι : Type*} [Finite ι] {ι' : Type w} (x : ι → R) (hi : ∀ i, x i ∈ I)
(f : (ι → R) →ₗ[R] ι' → R) (i : ι') : f x i ∈ I := by
classical
cases nonempty_fintype ι
rw [pi_eq_sum_univ x]
simp only [Finset.sum_apply, smul_eq_mul, map_sum, Pi.smul_apply, map_smul]
exact I.sum_mem fun j _ => I.mul_mem_right _ (hi j)
