restrictScalars_le_iff — Mathlib

English

For intermediate fields E1, E2 of L over E with a K-scalar tower, restrictScalars preserves order: E1.restrictScalars K ≤ E2.restrictScalars K iff E1 ≤ E2.

Русский

При наличии торового отношения скаляров ограничение скаляров сохраняет порядок: E1.restrictScalars K ≤ E2.restrictScalars K тогда и только тогда, когда E1 ≤ E2.

LaTeX

$$$E_1\restriction_K \le E_2\restriction_K \quad\iff\quad E_1 \le E_2$$$

Lean4

theorem restrictScalars_le_iff (K : Type*) {L E : Type*} [Field K] [Field L] [Field E] [Algebra K L] [Algebra K E]
    [Algebra L E] [IsScalarTower K L E] {E₁ E₂ : IntermediateField L E} :
    E₁.restrictScalars K ≤ E₂.restrictScalars K ↔ E₁ ≤ E₂ :=
  .rfl

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