instAddCommGroup — Mathlib

English

The additive structure on WeakBilin B is inherited from E; in particular WeakBilin B is an additive commutative group under the same operation as E.

Русский

Аддитивная структура WeakBilin B переходит из E; значит WeakBilin B образует коммутативную аддитивную группу с той же операцией сложения, что и в E.

LaTeX

$$WeakBilin B inherits the AddCommGroup structure from E, i.e., the addition is the same as on E.$$

Lean4

instance instAddCommGroup [CommSemiring 𝕜] [a : AddCommGroup E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F]
    (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) : AddCommGroup (WeakBilin B) :=
  a

Похожие утверждения