semilinearEquiv_apply — Mathlib

English

A simp lemma: equality of the underlying linear maps implies equality of the semilinear equivalences.

Русский

Утверждение-лемма: равенство базовых линейных отображений влечет равенство семилинейных эквивалентностей.

LaTeX

$${e1 e2} : (↑e1 : M →ₛₗ[σ] M₂) = e2 ↔ e1 = e2$$

Lean4

@[simp]
theorem _root_.SemilinearEquivClass.semilinearEquiv_apply {F : Type*} [EquivLike F M M₂] [SemilinearEquivClass F σ M M₂]
    (f : F) (x : M) : SemilinearEquivClass.semilinearEquiv (M₂ := M₂) f x = f x :=
  rfl

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