instIsSolvableTensorProduct — Mathlib

English

If L is solvable, then for any commutative algebra A over R, the tensor product A ⊗_R L is solvable.

Русский

Если L разрешима, то для любого A над R верно A ⊗_R L разрешимо.

LaTeX

$$$\text{IsSolvable } L \Rightarrow \text{IsSolvable } (A \otimes_R L)$$$

Lean4

instance {A : Type*} [CommRing A] [Algebra R A] [IsSolvable L] : IsSolvable (A ⊗[R] L) :=
  by
  obtain ⟨k, hk⟩ := IsSolvable.solvable R L
  rw [isSolvable_iff A]
  use k
  rw [derivedSeries_baseChange, hk, LieSubmodule.baseChange_bot]

Похожие утверждения