multiplicity_of_isUnit_right

Mathlib.RingTheory.Multiplicity

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

← MathLib Explorer

English

If a is not a unit and b is a unit, then multiplicity a b = 0.

Русский

Если a не единица, а b единица, то кратность a в b равна 0.

LaTeX

$$$(\neg \IsUnit(a)) \land \IsUnit(b) \Rightarrow \operatorname{multiplicity}(a,b) = 0$$$

Lean4

theorem multiplicity_of_isUnit_right {a b : α} (ha : ¬IsUnit a) (hb : IsUnit b) : multiplicity a b = 0 :=
  multiplicity_eq_zero.mpr fun h ↦ ha (isUnit_of_dvd_unit h hb)

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

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

Разделы

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

Аффилиация

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