coe_coe_ringHom — Mathlib

English

The coercion from OrderRingHom to RingHom is compatible with underlying function equality; i.e., the function part extracted from f as a RingHom is f.

Русский

Приведение из OrderRingHom к RingHom совместимо с равенством функций; то есть функция, извлечённая из f как RingHom, есть f.

LaTeX

$$$\\text{coe\_coe\_ringHom} : (f : \\alpha \\to+*o \\beta) \\mapsto (f : \\alpha \\to+* \\beta)$$$

Lean4

@[simp]
theorem coe_coe_ringHom (f : α →+*o β) : ⇑(f : α →+* β) = f :=
  rfl

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