ne_zero_of_mem_factors

Mathlib.RingTheory.UniqueFactorizationDomain.Defs

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

Lean4

theorem ne_zero_of_mem_factors {p a : α} (h : p ∈ factors a) : a ≠ 0 :=
  by
  rintro rfl
  simp at h

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

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

Разделы

Аффилиация

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