mk_coe — Mathlib

English

The construction that builds a LieDerivation from a linear map f and a compatibility condition h1 yields a LieDerivation whose underlying function is exactly f. Thus, the coercion from the paired data to a function is faithful.

Русский

Конструкция, превращающая линейное отображение f и условие совместимости h1 вLieDerivation, возвращаетLieDerivation, чья функция совпадает с f. Следовательно, приведение данных в функцию сохраняется корректно.

LaTeX

$$$((\langle f, h_1 \rangle : \text{LieDerivation } R\, L\, M) : L \to M) = f$$$

Lean4

@[simp]
theorem mk_coe (f : L →ₗ[R] M) (h₁) : ((⟨f, h₁⟩ : LieDerivation R L M) : L → M) = f :=
  rfl

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