adjoin_insert_intCast

Mathlib.Algebra.Algebra.Subalgebra.Lattice

URI: https://scilib.ai/kg/mathlib#Algebra.adjoin_insert_intCast

← MathLib Explorer

English

For any integer n and subset s, adjoin_R(insert n.cast s) = adjoin_R s.

Русский

Для целого n и множества s: adjoin_R(insert n.cast s) = adjoin_R s.

LaTeX

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

Lean4

@[simp]
theorem adjoin_insert_intCast (n : ℤ) (s : Set A) : adjoin R (insert (n : A) s) = adjoin R s := by
  simpa using adjoin_insert_algebraMap (n : R) s

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru