basisOfBasisLeft — Mathlib

English

If A and B are linearly disjoint with A ⊔ B = S, then there is a Basis of S over B obtained from a Basis of A by a suitable change of basis.

Русский

Если A и B линейно несовместны и A ⊔ B = S, то существует базис S как B-модуля, полученный из базиса A через подходящую замену базиса.

LaTeX

$$$H.basisOfBasisLeft H' b = \\text{basis of } S \\text{ over } B$$$

Lean4

/-- If `A` and `B` are subalgebras in a commutative algebra `S` over `R`, and if they are
linearly disjoint and such that `A ⊔ B = S`, then any `R`-basis of `A` is also a `B`-basis of `S`.
-/
noncomputable def basisOfBasisLeft (H' : A ⊔ B = ⊤) {ι : Type*} (b : Basis ι R A) : Basis ι B S :=
  (b.baseChange B).map (H.symm.mulMapLeftOfSupEqTop (by rwa [sup_comm])).toLinearEquiv

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