English
For all k, the k-th derived series computed over R and over ℤ have the same underlying set in L.
Русский
Для всех k геометрически k-я производящая серия, вычисленная над R и над ℤ, имеют одинаковое множество в L.
LaTeX
$$$(\mathrm{derivedSeries} \ R \ L \ k : Set\ L) = (\mathrm{derivedSeries} \ ℤ \ L \ k : Set\ L)$$$
Lean4
theorem coe_derivedSeries_eq_int (k : ℕ) : (derivedSeries R L k : Set L) = (derivedSeries ℤ L k : Set L) :=
by
rw [← LieSubmodule.coe_toSubmodule, ← LieSubmodule.coe_toSubmodule, derivedSeries_def, derivedSeries_def]
induction k with
| zero => rfl
| succ k ih =>
rw [derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_succ]
rw [LieSubmodule.lieIdeal_oper_eq_linear_span', LieSubmodule.lieIdeal_oper_eq_linear_span']
rw [Set.ext_iff] at ih
simp only [SetLike.mem_coe, LieSubmodule.mem_toSubmodule] at ih
simp only [ih]
apply le_antisymm
· exact coe_derivedSeries_eq_int_aux _ _ L k ih
· simp
