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