one_eq_closure

Mathlib.Algebra.Ring.Submonoid.Pointwise

URI: https://scilib.ai/kg/mathlib#AddSubmonoid.one_eq_closure

English

The unit 1 of AddSubmonoid R equals closure {1}.

Русский

Единица 1 подмодуля AddSubmonoid R равна замыканию множества {1}.

LaTeX

$$$1 : AddSubmonoid R = \mathrm{closure}\{1\}$$$

Lean4

theorem one_eq_closure : (1 : AddSubmonoid R) = closure { 1 } := by rw [closure_singleton_eq, one_eq_mrange]; congr 1;
  ext; simp

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

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

Разделы

Аффилиация

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