bilinear

Stream: Is there code for X?

[Patrick Massot]

Do we have the analogue of docs#linear_map.mk₂ for add_monoid_hom?

[Eric Wieser]

(linear_map.mk₂ ℕ _ _ _ _ _).to_add_monoid_hom, but that's probably very awkward

Edit: that doesn't even work

[Eric Wieser]

If we did it would be near here: https://leanprover-community.github.io/mathlib_docs/algebra/group/hom_instances.html#morphisms-of-morphisms