@[simp]

theorem LieAlgebra.comap_equiv_center {R : Type u_1} [CommRing R] {L : Type u_2} {L₂ : Type u_3} [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (e : L ≃ₗ⁅R⁆ L₂) : LieIdeal.comap e.toLieHom (center R L₂) = center R L

@[simp]

theorem LieAlgebra.map_equiv_center {R : Type u_1} [CommRing R] {L : Type u_2} {L₂ : Type u_3} [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (e : L ≃ₗ⁅R⁆ L₂) : LieIdeal.map e.toLieHom (center R L) = center R L₂