English
Let γ be a type with a multiplication. For any f: α → β and g1, g2, e1, e2: β → γ, the extension distributes over pointwise multiplication: extend f (g1 * g2) (e1 * e2) = extend f g1 e1 * extend f g2 e2.
Русский
Пусть γ имеет умножение. Пусть f: α → β и g1, g2, e1, e2: β → γ. Расширение по произведению и по соответствующим образом произведения возвращает произведение расширений: extend f (g1 * g2) (e1 * e2) = extend f g1 e1 * extend f g2 e2.
LaTeX
$$$ \mathrm{extend} f (g_1 * g_2) (e_1 * e_2) = \mathrm{extend} f g_1 e_1 * \mathrm{extend} f g_2 e_2 $$$
Lean4
@[to_additive]
theorem extend_mul [Mul γ] (f : α → β) (g₁ g₂ : α → γ) (e₁ e₂ : β → γ) :
Function.extend f (g₁ * g₂) (e₁ * e₂) = Function.extend f g₁ e₁ * Function.extend f g₂ e₂ := by
classical
funext x
simp [Function.extend_def, apply_dite₂]
