not_of_isUnit_left

Mathlib.RingTheory.Multiplicity

URI: https://scilib.ai/kg/mathlib#FiniteMultiplicity.not_of_isUnit_left

English

If a is a unit, then FiniteMultiplicity a b cannot hold for any b.

Русский

Если a является единицей, то для любого b не существует FiniteMultiplicity a b.

LaTeX

$$$ IsUnit(a) \Rightarrow \neg \operatorname{FiniteMultiplicity}(a,b) $$$

Lean4

@[simp]
theorem not_of_isUnit_left (b : α) (ha : IsUnit a) : ¬FiniteMultiplicity a b :=
  (·.not_unit ha)

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

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

Разделы

Аффилиация

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