revAtFun_inj

Mathlib.Algebra.Polynomial.Reverse

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

English

For each N, the map revAt N : ℕ → ℕ is injective.

Русский

Для каждого N отображение revAt N: ℕ → ℕ инъективно.

LaTeX

$$$\\forall a,b \\in \\mathbb{N},\\; \\mathrm{revAt}(N,a)=\\mathrm{revAt}(N,b) \\Rightarrow a=b.$$$

Lean4

theorem revAtFun_inj {N : ℕ} : Function.Injective (revAtFun N) :=
  by
  intro a b hab
  rw [← @revAtFun_invol N a, hab, revAtFun_invol]

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

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

Разделы

Аффилиация

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