coe_eq_one

Mathlib.Algebra.Algebra.Subalgebra.Basic

URI: https://scilib.ai/kg/mathlib#Subalgebra.coe_eq_one

English

The unit element 1 in S corresponds to the unit in A under the inclusion.

Русский

Единица в S соответствует единице в A через включение.

LaTeX

$${x ∈ S} : (x = 1) in A ⇔ (x = 1) in S$$

Lean4

protected theorem coe_eq_one {x : S} : (x : A) = 1 ↔ x = 1 :=
  OneMemClass.coe_eq_one

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

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

Разделы

Аффилиация

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