no goals
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι✝ : Type v
ι : Type u_1
inst✝ : Finite ι
ι' : Type w
x : ι → R
hi : ∀ (i : ι), x i ∈ I
f : (ι → R) →ₗ[R] ι' → R
i : ι'
⊢ ↑f x i ∈ I
classical
  cases nonempty_fintype ι
  rw [pi_eq_sum_univ x]
  simp only [Finset.sum_apply, smul_eq_mul, LinearMap.map_sum, Pi.smul_apply, LinearMap.map_smul]
  exact I.sum_mem fun j _ => I.mul_mem_right _ (hi j)
case intro
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι✝ : Type v
ι : Type u_1
inst✝ : Finite ι
ι' : Type w
x : ι → R
hi : ∀ (i : ι), x i ∈ I
f : (ι → R) →ₗ[R] ι' → R
i : ι'
val✝ : Fintype ι
⊢ ↑f x i ∈ I
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι✝ : Type v
ι : Type u_1
inst✝ : Finite ι
ι' : Type w
x : ι → R
hi : ∀ (i : ι), x i ∈ I
f : (ι → R) →ₗ[R] ι' → R
i : ι'
⊢ ↑f x i ∈ I
cases nonempty_fintype ι
case intro
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι✝ : Type v
ι : Type u_1
inst✝ : Finite ι
ι' : Type w
x : ι → R
hi : ∀ (i : ι), x i ∈ I
f : (ι → R) →ₗ[R] ι' → R
i : ι'
val✝ : Fintype ι
⊢ ↑f (∑ i : ι, x i • fun j => if i = j then 1 else 0) i ∈ I
case intro
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι✝ : Type v
ι : Type u_1
inst✝ : Finite ι
ι' : Type w
x : ι → R
hi : ∀ (i : ι), x i ∈ I
f : (ι → R) →ₗ[R] ι' → R
i : ι'
val✝ : Fintype ι
⊢ ↑f x i ∈ I
rw [pi_eq_sum_univ x]
case intro
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι✝ : Type v
ι : Type u_1
inst✝ : Finite ι
ι' : Type w
x : ι → R
hi : ∀ (i : ι), x i ∈ I
f : (ι → R) →ₗ[R] ι' → R
i : ι'
val✝ : Fintype ι
⊢ ∑ x_1 : ι, x x_1 * ↑f (fun j => if x_1 = j then 1 else 0) i ∈ I
case intro
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι✝ : Type v
ι : Type u_1
inst✝ : Finite ι
ι' : Type w
x : ι → R
hi : ∀ (i : ι), x i ∈ I
f : (ι → R) →ₗ[R] ι' → R
i : ι'
val✝ : Fintype ι
⊢ ↑f (∑ i : ι, x i • fun j => if i = j then 1 else 0) i ∈ I
simp only [Finset.sum_apply, smul_eq_mul, LinearMap.map_sum, Pi.smul_apply, LinearMap.map_smul]
no goals
case intro
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι✝ : Type v
ι : Type u_1
inst✝ : Finite ι
ι' : Type w
x : ι → R
hi : ∀ (i : ι), x i ∈ I
f : (ι → R) →ₗ[R] ι' → R
i : ι'
val✝ : Fintype ι
⊢ ∑ x_1 : ι, x x_1 * ↑f (fun j => if x_1 = j then 1 else 0) i ∈ I
exact I.sum_mem fun j _ => I.mul_mem_right _ (hi j)