coe_mk — Mathlib

English

The constructor AddChar.mk is id (for the underlying function): the coerced value matches the produced function.

Русский

Конструктор AddChar.mk совпадает с получаемой функцией: приводимая к функции величина равна самой функции.

LaTeX

$$$AddChar.mk f \; map_zero_eq_one' \; map_add_eq_mul' = f$$$

Lean4

@[simp]
theorem coe_mk (f : A → M) (map_zero_eq_one' : f 0 = 1) (map_add_eq_mul' : ∀ a b : A, f (a + b) = f a * f b) :
    AddChar.mk f map_zero_eq_one' map_add_eq_mul' = f := by rfl

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