not_of_unit_left

Mathlib.RingTheory.Multiplicity

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

English

For any a and unit u, FiniteMultiplicity u a is false.

Русский

Для любых a и единицы u, FiniteMultiplicity u a ложна.

LaTeX

$$$ \forall a,\forall u \,(\text{IsUnit}(u) \Rightarrow \neg \operatorname{FiniteMultiplicity}(u,a)) $$$

Lean4

theorem not_of_unit_left (a : α) (u : αˣ) : ¬FiniteMultiplicity (u : α) a :=
  FiniteMultiplicity.not_of_isUnit_left a u.isUnit

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

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

Разделы

Аффилиация

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