logEquiv_symm

Mathlib.Algebra.GroupWithZero.WithZero

URI: https://scilib.ai/kg/mathlib#WithZero.logEquiv_symm

English

The inverse of logEquiv is expEquiv; i.e., logEquiv^{-1} = expEquiv.

Русский

Обратное к logEquiv есть expEquiv; то есть logEquiv^{-1} = expEquiv.

LaTeX

$$$(\logEquiv)^{-1} = \expEquiv$$$

Lean4

@[simp]
theorem logEquiv_symm : (logEquiv (G := G)).symm = expEquiv :=
  rfl

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

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

Разделы

Аффилиация

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