logEquiv_apply

Mathlib.Algebra.GroupWithZero.WithZero

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

← MathLib Explorer

English

For every unit x in (Gᵐ⁰)ˣ, logEquiv x equals log x.

Русский

Для каждого элемента x из (Gᵐ⁰)ˣ выполняется logEquiv x = log x.

LaTeX

$$$\logEquiv(x) = \log x \quad (x \in (G^{\mathrm{m0}})^{\times})$$$

Lean4

@[simp]
theorem logEquiv_apply (x : (Gᵐ⁰)ˣ) : logEquiv x = log x :=
  by
  obtain ⟨_ | a, _ | b, hab, hba⟩ := x
  · cases hab
  · cases hab
  · cases hab
  · rfl

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

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

Разделы

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

Аффилиация

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