coe_algebraMap_over_bot — Mathlib

English

The algebra map from the bottom intermediate field to F coincides with the bottom equivalence.

Русский

Алгебраическое отображение из нижнего промежуточного поля в F совпадает с нижним эквивалентом.

LaTeX

$$$ (algebraMap (\\bot : \\text{IntermediateField}(F,E)) F : (\\bot : \\text{IntermediateField}(F,E)) \\to F) = botEquiv F E $$$

Lean4

theorem coe_algebraMap_over_bot :
    (algebraMap (⊥ : IntermediateField F E) F : (⊥ : IntermediateField F E) → F) = IntermediateField.botEquiv F E :=
  rfl

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