adjoin_insert_algebraMap — Mathlib

English

Inserting an algebraMap image into the generator set does not change the generated subalgebra: adjoin_R(insert(algebraMap_R A x) s) = adjoin_R s.

Русский

Добавление образа algebraMap не меняет порождение: adjoin_R(insert(algebraMap_R A x) s) = adjoin_R s.

LaTeX

$$$$\\operatorname{adjoin}_R(\\operatorname{insert}(\\operatorname{algebraMap}_R^A(x))\,s) = \\operatorname{adjoin}_R(s)$$$$

Lean4

@[simp]
theorem adjoin_insert_algebraMap (x : R) (s : Set A) : adjoin R (insert (algebraMap R A x) s) = adjoin R s :=
  by
  rw [Set.insert_eq, adjoin_union]
  simp

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