adjoin_singleton_intCast

Mathlib.Algebra.Algebra.Subalgebra.Lattice

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

English

For any integer n, adjoin_R{n.cast} equals the bottom subalgebra.

Русский

Для целого числа n порождение_R{n.cast} равно нулевой подалгебре.

LaTeX

$$$\\operatorname{adjoin}_R\\{(n : A)\\} = \\bot$$$

Lean4

@[simp]
theorem adjoin_singleton_intCast (n : ℤ) : adjoin R {(n : A)} = ⊥ := by
  simpa using adjoin_singleton_algebraMap A (n : R)

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

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

Разделы

Аффилиация

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