A : Type v
inst✝ : Ring A
h₁ : (IsCommutative A fun x x_1 => x * x_1) ↔ ∀ (a b : A), a * b = b * a
h₂ : IsLieAbelian A ↔ ∀ (a b : A), ⁅a, b⁆ = 0
⊢ (IsCommutative A fun x x_1 => x * x_1) ↔ IsLieAbelian A
A : Type v
inst✝ : Ring A
h₁ : (IsCommutative A fun x x_1 => x * x_1) ↔ ∀ (a b : A), a * b = b * a
⊢ (IsCommutative A fun x x_1 => x * x_1) ↔ IsLieAbelian A
have h₂ : IsLieAbelian A ↔ ∀ a b : A, ⁅a, b⁆ = 0 := ⟨fun h => h.1, fun h => ⟨h⟩⟩
no goals
A : Type v
inst✝ : Ring A
h₁ : (IsCommutative A fun x x_1 => x * x_1) ↔ ∀ (a b : A), a * b = b * a
h₂ : IsLieAbelian A ↔ ∀ (a b : A), ⁅a, b⁆ = 0
⊢ (IsCommutative A fun x x_1 => x * x_1) ↔ IsLieAbelian A
simp only [h₁, h₂, LieRing.of_associative_ring_bracket, sub_eq_zero]