expMonoidHom — Mathlib

English

Exponential function defines a monoid hom from the multiplicative real numbers to the real numbers.

Русский

Функция экспоненты задаёт тождество-моноидовую гомоморфную структуру от умножаемых действительных чисел к действительным.

LaTeX

$$$\\text{expMonoidHom} : (\\text{Multiplicative } \\mathbb{R}) \\to \\mathbb{R}$$$

Lean4

/-- the exponential function as a monoid hom from `Multiplicative ℝ` to `ℝ` -/
@[simps]
noncomputable def expMonoidHom : MonoidHom (Multiplicative ℝ) ℝ :=
  { toFun := fun x => exp x.toAdd, map_one' := by simp, map_mul' := by simp [exp_add] }

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