English
If α has an additive structure and coe to a function, then Multiplicative α coe to the same function.
Русский
Если у α есть аддитивная структура и существует вложение в функцию, то Multiplicative α тоже коэрцуется к той же функции.
LaTeX
$$$[\text{Additive } α]\ [\text{CoeFun } α β] \Rightarrow \mathrm{CoeFun}(\mathrm{Multiplicative } α)\ to\beta = \text{same as underlying}$$$
Lean4
/-- If `α` has some additive structure and coerces to a function,
then `Multiplicative α` should also coerce to the same function.
This allows `Multiplicative` to be used on bundled function types with an additive structure, which
is often used for composition, without affecting the behavior of the function itself.
-/
instance coeToFun {α : Type*} {β : α → Sort*} [CoeFun α β] : CoeFun (Multiplicative α) fun a => β a.toAdd :=
⟨fun a => CoeFun.coe a.toAdd⟩
