pow_prime_pow_mul_eq_one_iff

Mathlib.Algebra.CharP.Reduced

URI: https://scilib.ai/kg/mathlib#ExpChar.pow_prime_pow_mul_eq_one_iff

← MathLib Explorer

English

If R has CharP p, then any Subsemiring S of R also has CharP p.

Русский

Если у R характеристика p, то любой подпол semiring S кольца R также имеет CharP p.

LaTeX

$$$\\mathrm{CharP} S p$$$

Lean4

@[simp]
theorem pow_prime_pow_mul_eq_one_iff (p k m : ℕ) [ExpChar R p] (x : R) : x ^ (p ^ k * m) = 1 ↔ x ^ m = 1 :=
  by
  rw [pow_mul']
  convert ← (iterateFrobenius_inj R p k).eq_iff
  apply map_one

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

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

Разделы

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

Аффилиация

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