of_le_left — Mathlib

English

The left basis applied to index i equals the image of i under the left algebra map.

Русский

Применение левого базиса к индексу i равно образу i под левым алгебраическим отображением.

LaTeX

$$$H.basisOfBasisLeft H' b i = algebraMap A E (b i)$$$

Lean4

theorem of_le_left {A' : IntermediateField F E} (H : A.LinearDisjoint L) (h : A' ≤ A) : A'.LinearDisjoint L :=
  Subalgebra.LinearDisjoint.of_le_left_of_flat H h

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