adjoin_singleton_algebraMap — Mathlib

English

The subalgebra generated by a single algebra map image of R in A is the bottom subalgebra.

Русский

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

LaTeX

$$$$\\operatorname{adjoin}_R\\{\\operatorname{algebraMap}_R^A(x)\\} = \\bot$$$$

Lean4

@[simp]
theorem adjoin_singleton_algebraMap (x : R) : adjoin R {algebraMap R A x} = ⊥ :=
  bot_unique <| adjoin_singleton_le <| Subalgebra.algebraMap_mem _ _

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