Images of pairs of submodules under bilinear maps #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file provides
submodule.map₂, which is later used to implement
Main results #
This file is quite similar to the n-ary section of
data.set.basic and to
Please keep them in sync.
Map a pair of submodules under a bilinear map.
This is the submodule version of