toLinearEquivClass — Mathlib

English

From an AlgEquivClass F R A B one obtains a LinearEquivClass F R A B; equivalences are linear.

Русский

Из AlgEquivClass F R A B следует LinearEquivClass F R A B; эквивалентности линейны.

LaTeX

$$$\\text{LinearEquivClass } F\\; R\\; A\\; B$$$

Lean4

instance (priority := 100) toLinearEquivClass (F R A B : Type*) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A]
    [Algebra R B] [EquivLike F A B] [h : AlgEquivClass F R A B] : LinearEquivClass F R A B :=
  { h with map_smulₛₗ := fun f => map_smulₛₗ f }

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