∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] {N' : Type u_8} [inst_5 : AddCommGroup N'] [inst_6 : Module R N']
  (f : N →ₗ[R] N') (Q : QuadraticMap R M N), (f.compQuadraticMap' Q).polarBilin = LinearMap.compr₂ Q.polarBilin f