logEquiv_unitsMk0

Mathlib.Algebra.GroupWithZero.WithZero

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

English

The logEquiv sends the unit created by mk0 to the log of the underlying element.

Русский

logEquiv отдаёт единице mk0 логарифм основания x.

LaTeX

$$$\logEquiv(\mathrm{Units.mk0}(x,hx)) = \log x$$$

Lean4

theorem logEquiv_unitsMk0 (x : Gᵐ⁰) (hx) : logEquiv (.mk0 x hx) = log x :=
  logEquiv_apply _

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

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

Разделы

Аффилиация

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