adjoin_insert_natCast — Mathlib

English

Similarly, inserting a natCast n into s does not change the generated subalgebra: adjoin_R(insert(n) s) = adjoin_R s.

Русский

Вставка natCast не изменяет порождение: adjoin_R(insert(n) s) = adjoin_R s.

LaTeX

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

Lean4

@[simp]
theorem adjoin_insert_natCast (n : ℕ) (s : Set A) : adjoin R (insert (n : A) s) = adjoin R s :=
  mod_cast adjoin_insert_algebraMap (n : R) s

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