X_pow_mul_injective — Mathlib

English

Left-multiplication by X^k is injective on formal power series.

Русский

Левое умножение на X^k инъективно на формальных степенных рядах.

LaTeX

$$$\\forall R\\ [\\operatorname{Semiring} R], \\forall k \\in \\mathbb{N},\\ \\operatorname{Injective}(X^k \\cdot\\cdot): R\\llbracket X\\rrbracket \\to R\\llbracket X\\rrbracket$$$

Lean4

theorem X_pow_mul_injective {k : ℕ} : Function.Injective (X ^ k * · : R⟦X⟧ → R⟦X⟧) := fun _ _ ↦ X_pow_mul_cancel

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