coe_apply

Mathlib.Topology.Algebra.Module.Equiv

URI: https://scilib.ai/kg/mathlib#ContinuousLinearEquiv.coe_apply

English

For e: M₁ ≃SL[σ₁₂] M₂ and b ∈ M₁, the application of e as a map equals e(b).

Русский

Для e: M₁ ≃SL[σ₁₂] M₂ и b ∈ M₁, применение e как отображения равно e(b).

LaTeX

$$$ (e : M₁ \toSL[σ₁₂] M₂) \, b = e(b) $$$

Lean4

theorem coe_apply (e : M₁ ≃SL[σ₁₂] M₂) (b : M₁) : (e : M₁ →SL[σ₁₂] M₂) b = e b :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru