prime_p

Mathlib.NumberTheory.Padics.PadicIntegers

URI: https://scilib.ai/kg/mathlib#PadicInt.prime_p

English

The element p is a prime element in Z_p (the ideal it generates is prime).

Русский

Элемент p является простым элементом в Z_p (генерируемый им идеал прост).

LaTeX

$$Prime(p in ℤ_[p]).$$

Lean4

theorem prime_p : Prime (p : ℤ_[p]) :=
  by
  rw [← Ideal.span_singleton_prime, ← maximalIdeal_eq_span_p]
  · infer_instance
  · exact NeZero.ne _

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

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

Разделы

Аффилиация

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