coe_ofCoalgHom — Mathlib

English

The forward map of CoalgEquiv.ofCoalgHom f g h₁ h₂ is f; i.e., the resulting equivalence uses f as its forward direction.

Русский

Передающее отображение CoalgEquiv.ofCoalgHom f g h₁ h₂ равно f; то есть получившаяся эквивалентность использует f в качестве прямого направления.

LaTeX

$$$\\mathrm{ofCoalgHom}(f,g,h_1,h_2) = f$$$

Lean4

@[simp]
theorem coe_ofCoalgHom (f : A →ₗc[R] B) (g : B →ₗc[R] A) (h₁ h₂) : ofCoalgHom f g h₁ h₂ = f :=
  rfl

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