not_irreducible_zero

Mathlib.Algebra.Prime.Defs

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

← MathLib Explorer

English

If p is irreducible and u is a unit, p does not divide u.

Русский

Если p несводимо, и u — единица, то p не делит u.

LaTeX

$$¬ p \mid u$$

Lean4

@[simp]
theorem not_irreducible_zero [MonoidWithZero M] : ¬Irreducible (0 : M)
  | ⟨hn0, h⟩ =>
    have : IsUnit (0 : M) ∨ IsUnit (0 : M) := h (mul_zero 0).symm
    this.elim hn0 hn0

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

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

Разделы

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

Аффилиация

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