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
k : ℕ
⊢ derivedSeriesOfIdeal R L k I ≤ I
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
k : ℕ
⊢ map (incl I) (derivedSeries R { x // x ∈ ↑I } k) = derivedSeriesOfIdeal R L k I
rw [derivedSeries_eq_derivedSeriesOfIdeal_comap, map_comap_incl, inf_eq_right]
no goals
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
k : ℕ
⊢ derivedSeriesOfIdeal R L k I ≤ I
apply derivedSeriesOfIdeal_le_self