English
Let E, F be modules over 𝕜 with a bilinear B: E × F → 𝕜. If 𝕝 is another semiring acting on E compatibly, then WeakBilin B carries a natural Module 𝕝-structure induced from E (i.e., a module structure over 𝕝 is transported to WeakBilin B).
Русский
Пусть E, F — модули над 𝕜 и задан билинейной формой B: E × F → 𝕜. Если на E действует другой полемный полупределённый полумодуль 𝕝 совместно с 𝕜, то WeakBilin B естественным образом становится модулем над 𝕝, наследуя структуру модульности от E.
LaTeX
$$WeakBilin B is a module over 𝕝, via the underlying module structure on E transported along B.$$
Lean4
instance (priority := 100) instModule' [CommSemiring 𝕜] [CommSemiring 𝕝] [AddCommMonoid E] [Module 𝕜 E]
[AddCommMonoid F] [Module 𝕜 F] [m : Module 𝕝 E] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) : Module 𝕝 (WeakBilin B) :=
m
