R : Type u
ι : Type v
inst✝³ : CommRing R
L : ι → Type w
inst✝² : (i : ι) → LieRing (L i)
inst✝¹ : (i : ι) → LieAlgebra R (L i)
inst✝ : DecidableEq ι
i j : ι
hij : j ≠ i
x : L i
y : L j
⊢ ∀ (i_1 : ι), ↑(lieAlgebraComponent R ι L i_1) ⁅↑(of L i) x, ↑(of L j) y⁆ = ↑(lieAlgebraComponent R ι L i_1) 0
R : Type u
ι : Type v
inst✝³ : CommRing R
L : ι → Type w
inst✝² : (i : ι) → LieRing (L i)
inst✝¹ : (i : ι) → LieAlgebra R (L i)
inst✝ : DecidableEq ι
i j : ι
hij : j ≠ i
x : L i
y : L j
⊢ ⁅↑(of L i) x, ↑(of L j) y⁆ = 0
apply lieAlgebra_ext R ι L
R : Type u
ι : Type v
inst✝³ : CommRing R
L : ι → Type w
inst✝² : (i : ι) → LieRing (L i)
inst✝¹ : (i : ι) → LieAlgebra R (L i)
inst✝ : DecidableEq ι
i j : ι
hij : j ≠ i
x : L i
y : L j
k : ι
⊢ ↑(lieAlgebraComponent R ι L k) ⁅↑(of L i) x, ↑(of L j) y⁆ = ↑(lieAlgebraComponent R ι L k) 0
R : Type u
ι : Type v
inst✝³ : CommRing R
L : ι → Type w
inst✝² : (i : ι) → LieRing (L i)
inst✝¹ : (i : ι) → LieAlgebra R (L i)
inst✝ : DecidableEq ι
i j : ι
hij : j ≠ i
x : L i
y : L j
⊢ ∀ (i_1 : ι), ↑(lieAlgebraComponent R ι L i_1) ⁅↑(of L i) x, ↑(of L j) y⁆ = ↑(lieAlgebraComponent R ι L i_1) 0
intro k
R : Type u
ι : Type v
inst✝³ : CommRing R
L : ι → Type w
inst✝² : (i : ι) → LieRing (L i)
inst✝¹ : (i : ι) → LieAlgebra R (L i)
inst✝ : DecidableEq ι
i j : ι
hij : j ≠ i
x : L i
y : L j
k : ι
⊢ ⁅↑(lieAlgebraComponent R ι L k) (↑(of L i) x), ↑(lieAlgebraComponent R ι L k) (↑(of L j) y)⁆ =
    ↑(lieAlgebraComponent R ι L k) 0
R : Type u
ι : Type v
inst✝³ : CommRing R
L : ι → Type w
inst✝² : (i : ι) → LieRing (L i)
inst✝¹ : (i : ι) → LieAlgebra R (L i)
inst✝ : DecidableEq ι
i j : ι
hij : j ≠ i
x : L i
y : L j
k : ι
⊢ ↑(lieAlgebraComponent R ι L k) ⁅↑(of L i) x, ↑(of L j) y⁆ = ↑(lieAlgebraComponent R ι L k) 0
rw [LieHom.map_lie]
R : Type u
ι : Type v
inst✝³ : CommRing R
L : ι → Type w
inst✝² : (i : ι) → LieRing (L i)
inst✝¹ : (i : ι) → LieAlgebra R (L i)
inst✝ : DecidableEq ι
i j : ι
hij : j ≠ i
x : L i
y : L j
k : ι
⊢ ⁅if h : i = k then (_ : i = k) ▸ x else 0, if h : j = k then (_ : j = k) ▸ y else 0⁆ = 0
R : Type u
ι : Type v
inst✝³ : CommRing R
L : ι → Type w
inst✝² : (i : ι) → LieRing (L i)
inst✝¹ : (i : ι) → LieAlgebra R (L i)
inst✝ : DecidableEq ι
i j : ι
hij : j ≠ i
x : L i
y : L j
k : ι
⊢ ⁅↑(lieAlgebraComponent R ι L k) (↑(of L i) x), ↑(lieAlgebraComponent R ι L k) (↑(of L j) y)⁆ =
    ↑(lieAlgebraComponent R ι L k) 0
simp only [of, singleAddHom, AddMonoidHom.coe_mk, ZeroHom.coe_mk, lieAlgebraComponent_apply,
  component, lapply, LinearMap.coe_mk, AddHom.coe_mk, single_apply, LieHom.map_zero]
case pos
R : Type u
ι : Type v
inst✝³ : CommRing R
L : ι → Type w
inst✝² : (i : ι) → LieRing (L i)
inst✝¹ : (i : ι) → LieAlgebra R (L i)
inst✝ : DecidableEq ι
i j : ι
hij : j ≠ i
x : L i
y : L j
k : ι
hik : i = k
⊢ ⁅if h : i = k then (_ : i = k) ▸ x else 0, if h : j = k then (_ : j = k) ▸ y else 0⁆ = 0

case neg
R : Type u
ι : Type v
inst✝³ : CommRing R
L : ι → Type w
inst✝² : (i : ι) → LieRing (L i)
inst✝¹ : (i : ι) → LieAlgebra R (L i)
inst✝ : DecidableEq ι
i j : ι
hij : j ≠ i
x : L i
y : L j
k : ι
hik : ¬i = k
⊢ ⁅if h : i = k then (_ : i = k) ▸ x else 0, if h : j = k then (_ : j = k) ▸ y else 0⁆ = 0
R : Type u
ι : Type v
inst✝³ : CommRing R
L : ι → Type w
inst✝² : (i : ι) → LieRing (L i)
inst✝¹ : (i : ι) → LieAlgebra R (L i)
inst✝ : DecidableEq ι
i j : ι
hij : j ≠ i
x : L i
y : L j
k : ι
⊢ ⁅if h : i = k then (_ : i = k) ▸ x else 0, if h : j = k then (_ : j = k) ▸ y else 0⁆ = 0
by_cases hik : i = k
no goals
case pos
R : Type u
ι : Type v
inst✝³ : CommRing R
L : ι → Type w
inst✝² : (i : ι) → LieRing (L i)
inst✝¹ : (i : ι) → LieAlgebra R (L i)
inst✝ : DecidableEq ι
i j : ι
hij : j ≠ i
x : L i
y : L j
k : ι
hik : i = k
⊢ ⁅if h : i = k then (_ : i = k) ▸ x else 0, if h : j = k then (_ : j = k) ▸ y else 0⁆ = 0
simp only [dif_neg, not_false_iff, lie_zero, hik.symm, hij]
no goals
case neg
R : Type u
ι : Type v
inst✝³ : CommRing R
L : ι → Type w
inst✝² : (i : ι) → LieRing (L i)
inst✝¹ : (i : ι) → LieAlgebra R (L i)
inst✝ : DecidableEq ι
i j : ι
hij : j ≠ i
x : L i
y : L j
k : ι
hik : ¬i = k
⊢ ⁅if h : i = k then (_ : i = k) ▸ x else 0, if h : j = k then (_ : j = k) ▸ y else 0⁆ = 0
simp only [dif_neg, not_false_iff, zero_lie, hik]