of_basis_right' — Mathlib

English

Coordinates under the right basis representation correspond via the algebra map to coordinates of the original basis.

Русский

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

LaTeX

$$$(H.basisOfBasisRight H' b).repr x i) = (algebraMap ...)(b.repr x i)$$$

Lean4

/-- If there exists an `F`-basis of `L` which remains linearly independent over `A`, then
`A` and `L` are linearly disjoint. -/
theorem of_basis_right' {ι : Type*} (b : Basis ι F L) (H : LinearIndependent A (algebraMap L E ∘ b)) :
    A.LinearDisjoint L :=
  Subalgebra.LinearDisjoint.of_basis_right _ _
    (b.map (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).toLinearEquiv) H

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