coe_inj — Mathlib

English

For polynomials φ, ψ, we have (φ : PowerSeries R) = ψ ↔ φ = ψ; i.e., the embedding is faithful.

Русский

Для полиномов φ, ψ имеет место эквивалентность (φ : PowerSeries R) = ψ ↔ φ = ψ; вложение верно сохраняет различия.

LaTeX

$$$(\\varphi : PowerSeries R) = \\psi \\ \\iff \\ \\varphi = \\psi$$$

Lean4

@[simp, norm_cast]
theorem coe_inj : (φ : PowerSeries R) = ψ ↔ φ = ψ :=
  (coe_injective R).eq_iff

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