map_bot — Mathlib

English

For any F-algebra hom f: E →ₐ[F] K, the image of the bottom intermediate field under map f is the bottom intermediate field in K.

Русский

Для любого гомоморфизма алгебр F-E → F-K карта f отображает нижнее промежуточное поле в ноль: map f ⊥ = ⊥.

LaTeX

$$$\operatorname{map}(f, \bot) = \bot$$$

Lean4

@[simp]
theorem map_bot (f : E →ₐ[F] K) : IntermediateField.map f ⊥ = ⊥ :=
  toSubalgebra_injective <| Algebra.map_bot _

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