theorem LieRing.mul_lie_of_associative {A : Type u_2} [Ring A] (x y z : A) : ⁅x * y, z⁆ = ⁅x, z⁆ * y + x * ⁅y, z⁆

theorem LieRing.list_prod_ofFn_lie_of_associative {A : Type u_2} [Ring A] {n : ℕ} (f : Fin n → A) (x : A) : ⁅(List.ofFn f).prod, x⁆ = ∑ i : Fin n, (List.ofFn (Function.update f i ⁅f i, x⁆)).prod

instance LieRing.instIsLieAbelian_ado {A : Type u_4} [CommRing A] : IsLieAbelian A