case intro.intro
n : Type u_1
p : Type ?u.17923
q : Type ?u.17926
l : Type ?u.17929
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Nontrivial R
h : 1 < Fintype.card n
j i : n
hij : j ≠ i
⊢ ¬IsLieAbelian { x // x ∈ sl n R }
n : Type u_1
p : Type ?u.17923
q : Type ?u.17926
l : Type ?u.17929
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Nontrivial R
h : 1 < Fintype.card n
⊢ ¬IsLieAbelian { x // x ∈ sl n R }
rcases Fintype.exists_pair_of_one_lt_card h with ⟨j, i, hij⟩
case intro.intro
n : Type u_1
p : Type ?u.17923
q : Type ?u.17926
l : Type ?u.17929
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Nontrivial R
h : 1 < Fintype.card n
j i : n
hij : j ≠ i
A : { x // x ∈ sl n R } := Eb R i j hij
⊢ ¬IsLieAbelian { x // x ∈ sl n R }
case intro.intro
n : Type u_1
p : Type ?u.17923
q : Type ?u.17926
l : Type ?u.17929
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Nontrivial R
h : 1 < Fintype.card n
j i : n
hij : j ≠ i
⊢ ¬IsLieAbelian { x // x ∈ sl n R }
let A := Eb R i j hij
case intro.intro
n : Type u_1
p : Type ?u.17923
q : Type ?u.17926
l : Type ?u.17929
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Nontrivial R
h : 1 < Fintype.card n
j i : n
hij : j ≠ i
A : { x // x ∈ sl n R } := Eb R i j hij
B : { x // x ∈ sl n R } := Eb R j i (_ : i ≠ j)
⊢ ¬IsLieAbelian { x // x ∈ sl n R }
case intro.intro
n : Type u_1
p : Type ?u.17923
q : Type ?u.17926
l : Type ?u.17929
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Nontrivial R
h : 1 < Fintype.card n
j i : n
hij : j ≠ i
A : { x // x ∈ sl n R } := Eb R i j hij
⊢ ¬IsLieAbelian { x // x ∈ sl n R }
let B := Eb R j i hij.symm
case intro.intro
n : Type u_1
p : Type ?u.17923
q : Type ?u.17926
l : Type ?u.17929
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Nontrivial R
h : 1 < Fintype.card n
j i : n
hij : j ≠ i
A : { x // x ∈ sl n R } := Eb R i j hij
B : { x // x ∈ sl n R } := Eb R j i (_ : i ≠ j)
c : IsLieAbelian { x // x ∈ sl n R }
⊢ False
case intro.intro
n : Type u_1
p : Type ?u.17923
q : Type ?u.17926
l : Type ?u.17929
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Nontrivial R
h : 1 < Fintype.card n
j i : n
hij : j ≠ i
A : { x // x ∈ sl n R } := Eb R i j hij
B : { x // x ∈ sl n R } := Eb R j i (_ : i ≠ j)
⊢ ¬IsLieAbelian { x // x ∈ sl n R }
intro c
case intro.intro
n : Type u_1
p : Type ?u.17923
q : Type ?u.17926
l : Type ?u.17929
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Nontrivial R
h : 1 < Fintype.card n
j i : n
hij : j ≠ i
A : { x // x ∈ sl n R } := Eb R i j hij
B : { x // x ∈ sl n R } := Eb R j i (_ : i ≠ j)
c : IsLieAbelian { x // x ∈ sl n R }
c' : ↑A ⬝ ↑B = ↑B ⬝ ↑A
⊢ False
case intro.intro
n : Type u_1
p : Type ?u.17923
q : Type ?u.17926
l : Type ?u.17929
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Nontrivial R
h : 1 < Fintype.card n
j i : n
hij : j ≠ i
A : { x // x ∈ sl n R } := Eb R i j hij
B : { x // x ∈ sl n R } := Eb R j i (_ : i ≠ j)
c : IsLieAbelian { x // x ∈ sl n R }
⊢ False
have c' : A.val ⬝ B.val = B.val ⬝ A.val := by
  rw [← sub_eq_zero, ← sl_bracket, c.trivial, ZeroMemClass.coe_zero]
no goals
case intro.intro
n : Type u_1
p : Type ?u.17923
q : Type ?u.17926
l : Type ?u.17929
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Nontrivial R
h : 1 < Fintype.card n
j i : n
hij : j ≠ i
A : { x // x ∈ sl n R } := Eb R i j hij
B : { x // x ∈ sl n R } := Eb R j i (_ : i ≠ j)
c : IsLieAbelian { x // x ∈ sl n R }
c' : ↑A ⬝ ↑B = ↑B ⬝ ↑A
⊢ False
simpa [stdBasisMatrix, Matrix.mul_apply, hij] using congr_fun (congr_fun c' i) i
no goals
n : Type u_1
p : Type ?u.17923
q : Type ?u.17926
l : Type ?u.17929
R : Type u₂
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq l
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Nontrivial R
h : 1 < Fintype.card n
j i : n
hij : j ≠ i
A : { x // x ∈ sl n R } := Eb R i j hij
B : { x // x ∈ sl n R } := Eb R j i (_ : i ≠ j)
c : IsLieAbelian { x // x ∈ sl n R }
⊢ ↑A ⬝ ↑B = ↑B ⬝ ↑A
rw [← sub_eq_zero, ← sl_bracket, c.trivial, ZeroMemClass.coe_zero]