feat(algebra/group/type_tags): adding function coercion for `additive…

…` and `multiplicative` (#6657)

[As on zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/to_additive.20mismatch/near/230042978)




Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/algebra/group/type_tags.lean

@@ -242,3 +242,23 @@ def add_monoid_hom.to_multiplicative'' [add_monoid α] [monoid β] :
 def monoid_hom.to_additive'' [add_monoid α] [monoid β] :
   (multiplicative α →* β) ≃ (α →+ additive β) :=
 add_monoid_hom.to_multiplicative''.symm
+
+/-- 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 additive.has_coe_to_fun {α : Type*} [has_coe_to_fun α] :
+  has_coe_to_fun (additive α) :=
+⟨λ a, has_coe_to_fun.F a.to_mul, λ a, coe_fn a.to_mul⟩
+
+/-- 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 multiplicative.has_coe_to_fun {α : Type*} [has_coe_to_fun α] :
+  has_coe_to_fun (multiplicative α) :=
+⟨λ a, has_coe_to_fun.F a.to_add, λ a, coe_fn a.to_add⟩