coe_orderMonoidWithZeroHom_apply — Mathlib

English

For f: α →+*o β and a ∈ α, the value of the underlying alpha-to-zero monoid-with-zero map equals f a; i.e., (f : α →*₀o β) a = f a.

Русский

Для f: α →+*o β и a ∈ α значение соответствующего отображения α →*₀o β равно f(a); то есть (f : α →*₀o β) a = f a.

LaTeX

$$$ (f : α \\to*₀o β) \\, a = f(a) $$$

Lean4

@[norm_cast]
theorem coe_orderMonoidWithZeroHom_apply (f : α →+*o β) (a : α) : (f : α →*₀o β) a = f a :=
  rfl

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