LinearDisjoint — Mathlib

English

Two intermediate fields are linearly disjoint if and only if they are linearly disjoint as subalgebras.

Русский

Два промежуточных поля линейно не пересекаются тогда и только тогда, когда они линейно не пересекаются как подалгебры.

LaTeX

$$$A \\text{ LinearDisjoint } B \\;\\iff\\; A^{\\text{toSubalgebra}} \\text{ LinearDisjoint } B^{\\text{toSubalgebra}}.$$$

Lean4

/-- If `A` is an intermediate field of `E / F`, and `E / L / F` is a field extension tower,
then `A` and `L` are linearly disjoint, if they are linearly disjoint as subalgebras of `E`
(`Subalgebra.LinearDisjoint`). -/
protected abbrev LinearDisjoint : Prop :=
  A.toSubalgebra.LinearDisjoint (IsScalarTower.toAlgHom F L E).range

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