coeff_injective

Mathlib.RingTheory.HahnSeries.Basic

URI: https://scilib.ai/kg/mathlib#HahnSeries.coeff_injective

English

The coefficient map x ↦ x.coeff is injective on HahnSeries Γ R.

Русский

Коэффициентное отображение x ↦ x.coeff инъективно на HahnSeries Γ R.

LaTeX

$$$\\text{coeff}: HahnSeries(\\Gamma, R) \\to (\\Gamma \\to R) \\text{ is injective}$$$

Lean4

theorem coeff_injective : Injective (coeff : HahnSeries Γ R → Γ → R) := fun _ _ => HahnSeries.ext

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru