of_le_right' — Mathlib

English

If A is linearly disjoint from B and B′ ⊆ B, then A is linearly disjoint from B′.

Русский

Если A линейно разобщено с B, и B' ⊆ B, то A разобщено с B'.

LaTeX

$$$A' \perp B' \text{ if } A' ≤ A, B' ≤ B$$$

Lean4

/-- Similar to `IntermediateField.LinearDisjoint.of_le_right` but this is for abstract fields. -/
theorem of_le_right' (H : A.LinearDisjoint L) (L' : Type*) [Field L'] [Algebra F L'] [Algebra L' L]
    [IsScalarTower F L' L] [Algebra L' E] [IsScalarTower F L' E] [IsScalarTower L' L E] : A.LinearDisjoint L' :=
  by
  refine Subalgebra.LinearDisjoint.of_le_right_of_flat H ?_
  convert AlgHom.range_comp_le_range (IsScalarTower.toAlgHom F L' L) (IsScalarTower.toAlgHom F L E)
  ext; exact IsScalarTower.algebraMap_apply L' L E _

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