extendScalars_inf — Mathlib

English

If h: F ≤ E and h': F ≤ E' are inclusions of an intermediate field F, then the meet of their extensions equals the extension of the meet: extendScalars h ⊓ extendScalars h' = extendScalars (le_inf h h').

Русский

Если F ≤ E и F ≤ E' — два промежуточных поля, то пересечение их расширений скаляров равно расширению пересечения: extendScalars h ⊓ extendScalars h' = extendScalars (le_inf h h').

LaTeX

$$$ (\operatorname{extendScalars} h) \;\sqcap\; (\operatorname{extendScalars} h') = \operatorname{extendScalars}(\,\operatorname{le\_inf}(h,h')\,),$$$

Lean4

theorem extendScalars_inf : extendScalars h ⊓ extendScalars h' = extendScalars (le_inf h h') :=
  ((extendScalars.orderIso F).map_inf ⟨_, h⟩ ⟨_, h'⟩).symm

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