X_mul_inj — Mathlib

English

Multiplication by X is injective on formal power series over a semiring: if X·φ = X·ψ, then φ = ψ.

Русский

Умножение на X инъективно на пространстве формальных степенных рядов над полупрямым кольцом: если X·φ = X·ψ, то φ = ψ.

LaTeX

$$$\\forall R\\ [\\operatorname{Semiring} R], \\ \\forall \\phi, \\psi \\in R\\llbracket X\\rrbracket,\ \ X\\phi = X\\psi \\Longrightarrow \\phi = \\psi$$$

Lean4

theorem X_mul_inj {φ ψ : R⟦X⟧} : X * φ = X * ψ ↔ φ = ψ :=
  X_mul_injective.eq_iff

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