expand_injective

Mathlib.Algebra.Polynomial.Expand

URI: https://scilib.ai/kg/mathlib#Polynomial.expand_injective

← MathLib Explorer

English

If p > 0, then the expansion map expand R p is injective.

Русский

Если p > 0, то отображение expansion R p инъективно.

LaTeX

$$$\text{Injective}(\mathrm{expand}\; R\; p)$$$

Lean4

/-- Expansion is injective. -/
theorem expand_injective {n : ℕ} (hn : 0 < n) : Function.Injective (expand R n) := fun g g' H =>
  ext fun k => by rw [← coeff_expand_mul hn, H, coeff_expand_mul hn]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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