mem_restrict — Mathlib

English

The restrict_algEquiv construction provides an algebra equivalence between F and the restricted field, i.e., F ≃ₐ[K] ↥(IntermediateField.restrict h).

Русский

Конструкция restrict_algEquiv обеспечивает алгебраическое эквивалентство между F и ограниченным полем, т.е. F ≃ₐ[K] ↥(IntermediateField.restrict h).

LaTeX

$$$F \\cong_K \\mathrm{IntermediateField}(K, E) \\text{ via } \\text{restrict\_algEquiv}(h)$$$

Lean4

theorem mem_restrict (x : E) : x ∈ restrict h ↔ x.1 ∈ F :=
  Set.ext_iff.mp (Set.range_inclusion h) x

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