isUnit_exp

Mathlib.RingTheory.Nilpotent.Exp

URI: https://scilib.ai/kg/mathlib#IsNilpotent.isUnit_exp

← MathLib Explorer

English

If a is nilpotent in a ring, then exp(a) is a unit; in particular exp(a) has inverse exp(−a).

Русский

Если a нильпотентен в кольце, то exp(a) является единицей (имеет обратное exp(−a)).

LaTeX

$$$\mathrm{IsUnit}(\exp(a))$$$

Lean4

theorem isUnit_exp {a : A} (h : IsNilpotent a) : IsUnit (exp a) :=
  by
  apply isUnit_iff_exists.2
  use exp (-a)
  exact ⟨exp_mul_exp_neg_self h, exp_neg_mul_exp_self h⟩

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

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

Разделы

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

Аффилиация

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