isLinear — Mathlib

English

A trivialization e induces a linear structure on the associated pretrivialization; in particular, e.toPretrivialization is linear with respect to R.

Русский

Тривиализация e порождает линейную структуру у соответствующей предтривиализации; в частности, e.toPretrivialization линейна по координате R.

LaTeX

$$$ e.toPretrivialization.\text{IsLinear } R \\text{ holds}.$$

Lean4

instance isLinear [AddCommMonoid F] [Module R F] [∀ x, AddCommMonoid (E x)] [∀ x, Module R (E x)] [e.IsLinear R] :
    e.toPretrivialization.IsLinear R :=
  { (‹_› : e.IsLinear R) with }

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