case pos
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M₃
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
f : (i : ι) → M₂ →ₗ[R] φ i
c : M₂
i j : ι
b : M₂ →ₗ[R] φ i
h : j = i
⊢ ↑(update f i b j) c = update (fun i => ↑(f i) c) i (↑b c) j

case neg
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M₃
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
f : (i : ι) → M₂ →ₗ[R] φ i
c : M₂
i j : ι
b : M₂ →ₗ[R] φ i
h : ¬j = i
⊢ ↑(update f i b j) c = update (fun i => ↑(f i) c) i (↑b c) j
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M₃
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
f : (i : ι) → M₂ →ₗ[R] φ i
c : M₂
i j : ι
b : M₂ →ₗ[R] φ i
⊢ ↑(update f i b j) c = update (fun i => ↑(f i) c) i (↑b c) j
by_cases h : j = i
no goals
case pos
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M₃
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
f : (i : ι) → M₂ →ₗ[R] φ i
c : M₂
i j : ι
b : M₂ →ₗ[R] φ i
h : j = i
⊢ ↑(update f i b j) c = update (fun i => ↑(f i) c) i (↑b c) j
rw [h, update_same, update_same]
no goals
case neg
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M₃
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
f : (i : ι) → M₂ →ₗ[R] φ i
c : M₂
i j : ι
b : M₂ →ₗ[R] φ i
h : ¬j = i
⊢ ↑(update f i b j) c = update (fun i => ↑(f i) c) i (↑b c) j
rw [update_noteq h, update_noteq h]