coe_inj — Mathlib

English

Two arithmetic functions are equal iff their coercions to functions agree; i.e., the coercion map is injective.

Русский

Две арифметические функции равны тогда и только тогда, когда их приведение к функциям согласуется; то есть коэрцирование инъективно.

LaTeX

$$$(f : \\mathbb{N} \\to R) = g \\;\\Longleftrightarrow\\; f = g$$$

Lean4

theorem coe_inj {f g : ArithmeticFunction R} : (f : ℕ → R) = g ↔ f = g :=
  DFunLike.coe_fn_eq

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