ne_zero_of_mem_factors

Mathlib.RingTheory.PrincipalIdealDomain

URI: https://scilib.ai/kg/mathlib#PrincipalIdealRing.ne_zero_of_mem_factors

← MathLib Explorer

English

If a ≠ 0 and b is a factor of a, then b ≠ 0.

Русский

Если a ≠ 0 и b делит a, то b ≠ 0.

LaTeX

$$$a \\neq 0 \\rightarrow b \\in \\text{factors}(a) \\rightarrow b \\neq 0$$$

Lean4

theorem ne_zero_of_mem_factors {R : Type v} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {a b : R} (ha : a ≠ 0)
    (hb : b ∈ factors a) : b ≠ 0 :=
  Irreducible.ne_zero ((factors_spec a ha).1 b hb)

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

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

Разделы

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

Аффилиация

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