injective_pow_p

Mathlib.FieldTheory.Perfect

URI: https://scilib.ai/kg/mathlib#injective_pow_p

English

Let x,y ∈ R. If x^p = y^p, then x = y; i.e., the map x ↦ x^p is injective on R.

Русский

Пусть x,y ∈ R. Если x^p = y^p, то x = y; т.е. отображение x ↦ x^p инъективно.

LaTeX

$$$ \forall x,y\in R\, (x^p = y^p) \Rightarrow x = y. $$$

Lean4

theorem injective_pow_p {x y : R} (h : x ^ p = y ^ p) : x = y :=
  (frobeniusEquiv R p).injective h

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

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

Разделы

Аффилиация

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