case mp
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
e : L' ≃ₗ⁅R⁆ L
h : IsSolvable R L'
⊢ IsSolvable R L

case mpr
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
e : L' ≃ₗ⁅R⁆ L
h : IsSolvable R L
⊢ IsSolvable R L'
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
e : L' ≃ₗ⁅R⁆ L
⊢ IsSolvable R L' ↔ IsSolvable R L
constructor <;> intro h
no goals
case mp
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
e : L' ≃ₗ⁅R⁆ L
h : IsSolvable R L'
⊢ IsSolvable R L
exact e.symm.injective.lieAlgebra_isSolvable
no goals
case mpr
R : Type u
L : Type v
M : Type w
L' : Type w₁
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I J : LieIdeal R L
f : L' →ₗ⁅R⁆ L
e : L' ≃ₗ⁅R⁆ L
h : IsSolvable R L
⊢ IsSolvable R L'
exact e.injective.lieAlgebra_isSolvable