coe_mk — Mathlib

English

If you build a nonunital algebra homomorphism from f and witnesses h1–h4, its underlying fun is f.

Русский

Если построить гомоморфизм без единицы из функции f и доказательств h1–h4, то базовая функция совпадает с f.

LaTeX

$$$(\text{mk } f)\;\text{has underlying function } f$$$

Lean4

@[simp]
theorem coe_mk (f : A → B) (h₁ h₂ h₃ h₄) : ⇑(⟨⟨⟨f, h₁⟩, h₂, h₃⟩, h₄⟩ : A →ₛₙₐ[φ] B) = f :=
  rfl

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