linearDisjoint_iff' — Mathlib

English

Two intermediate fields are linearly disjoint iff their substituted subtype ranges are linearly disjoint.

Русский

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

LaTeX

$$$A.LinearDisjoint B \\iff A.toSubalgebra.LinearDisjoint B.toSubalgebra$ .$$

Lean4

/-- Two intermediate fields are linearly disjoint if and only if
they are linearly disjoint as subalgebras. -/
theorem linearDisjoint_iff' : A.LinearDisjoint B ↔ A.toSubalgebra.LinearDisjoint B.toSubalgebra :=
  by
  rw [linearDisjoint_iff]
  congr!
  ext; simp

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