adjoin_insert_zero — Mathlib

English

Inserting 0 into a generator set does not change the generated subalgebra: adjoin_R(insert(0) s) = adjoin_R s.

Русский

Добавление 0 в набор порождений не меняет порождение: adjoin_R(insert(0) s) = adjoin_R s.

LaTeX

$$$$\\operatorname{adjoin}_R(\\operatorname{insert}(0)\\,s) = \\operatorname{adjoin}_R(s)$$$$

Lean4

@[simp]
theorem adjoin_insert_zero (s : Set A) : adjoin R (insert 0 s) = adjoin R s :=
  mod_cast adjoin_insert_natCast R 0 s

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