mul_X_pow_injective — Mathlib

English

Left multiplication by X^k is injective on PowerSeries R.

Русский

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

LaTeX

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

Lean4

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

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