instFunLike — Mathlib

English

The collection of σ-semi-linear maps M →ₛₗ[σ] M3 is equipped with a SemilinearMapClass structure, where addition and scalar action operate pointwise, and evaluation uses the underlying function.

Русский

Множество σ-симилелинейных отображений M →ₛₗ[σ] M3 наделяется структурой класса полулинейных отображений, операция сложения и скалярного действия определены покомпонентно, а применение свершается через базовую функцию.

LaTeX

$$$\mathrm{SemilinearMapClass}\ (M \to_\sigma M_3)\ \sigma\ M\ M_3$$$

Lean4

instance instFunLike : FunLike (M →ₛₗ[σ] M₃) M M₃
    where
  coe f := f.toFun
  coe_injective' f g
    h := by
    cases f
    cases g
    congr
    apply DFunLike.coe_injective'
    exact h

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