one_def

Mathlib.Algebra.Group.TransferInstance

URI: https://scilib.ai/kg/mathlib#Equiv.one_def

English

Under the transported One via e, the equality 1 = e.symm 1 holds, i.e., 1_α = e^{-1}(1_β).

Русский

При переносе единицы через e выполняется равенство 1_α = e^{-1}(1_β).

LaTeX

$$$$1 = e^{-1}(1).$$$$

Lean4

@[to_additive]
theorem one_def [One β] :
    letI := e.one
    1 = e.symm 1 :=
  rfl

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

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

Разделы

Аффилиация

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