charP_iff_prime_eq_zero

Mathlib.Algebra.CharP.Basic

URI: https://scilib.ai/kg/mathlib#CharP.charP_iff_prime_eq_zero

← MathLib Explorer

English

For a prime p, CharP R p holds if and only if p maps to 0 in R.

Русский

Для простого p верно: CharP R p тогда и только тогда, когда p ↦ 0 в R.

LaTeX

$$$ \forall {R}, [Nontrivial R], [CharP R p] \iff (p : R) = 0 $$$

Lean4

theorem charP_iff_prime_eq_zero [Nontrivial R] {p : ℕ} (hp : p.Prime) : CharP R p ↔ (p : R) = 0 :=
  ⟨fun _ => cast_eq_zero R p, fun hp0 => (ringChar_of_prime_eq_zero hp hp0) ▸ inferInstance⟩

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

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

Разделы

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

Аффилиация

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