not_unit

Mathlib.RingTheory.Multiplicity

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

English

If FiniteMultiplicity a b holds, then a is not a unit.

Русский

Если FiniteMultiplicity a b, то a не является единицей.

LaTeX

$$$$FiniteMultiplicity\ a\ b \rightarrow \lnot IsUnit\ a.$$$$

Lean4

theorem not_unit (h : FiniteMultiplicity a b) : ¬IsUnit a :=
  let ⟨n, hn⟩ := h
  hn ∘ IsUnit.dvd ∘ IsUnit.pow (n + 1)

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

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

Разделы

Аффилиация

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