Biadditive maps as integer-bilinear maps

A biadditive map μ : M →+ N →+ P of additive commutative groups is ℤ-bilinear, since the ℤ-module structure of an additive group is its own addition. This file packages that as AddMonoidHom.toIntLinearMap₂, the two-variable counterpart of Mathlib's AddMonoidHom.toIntLinearMap, so that constructions stated for bilinear maps over a ring can be fed a biadditive pairing directly.

def AddMonoidHom.toIntLinearMap₂ {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] (μ : M →+ N →+ P) : M →ₗ[ℤ] N →ₗ[ℤ] P

Reinterpret a biadditive map as a ℤ-bilinear map.

Equations

• μ.toIntLinearMap₂ = LinearMap.mk₂ ℤ (fun (m : M) (n : N) => (μ m) n) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem AddMonoidHom.toIntLinearMap₂_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] (μ : M →+ N →+ P) (m : M) (n : N) : (μ.toIntLinearMap₂ m) n = (μ m) n