mk_coe — Mathlib

English

If you build an AlgHom by wrapping f with the same data that defined f, you recover f. The constructor is definitional.

Русский

Если собрать AlgHom с теми же данными, что определяли f, получится f. Конструктор задаётся определением.

LaTeX

$$$ ( ⟨⟨⟨⟨f, h_1⟩, h_2⟩, h_3, h_4⟩, h_5⟩ : A \\to_ R B ) = f $$$

Lean4

@[simp]
theorem mk_coe {f : A →ₐ[R] B} (h₁ h₂ h₃ h₄ h₅) : (⟨⟨⟨⟨f, h₁⟩, h₂⟩, h₃, h₄⟩, h₅⟩ : A →ₐ[R] B) = f :=
  rfl

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