not_dvd_of_one_right

Mathlib.RingTheory.Multiplicity

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

← MathLib Explorer

English

If FiniteMultiplicity a 1 holds, then a does not divide 1.

Русский

Если FiniteMultiplicity a 1 выполняется, то a не делит 1.

LaTeX

$$$$FiniteMultiplicity\ a\ 1 \rightarrow \lnot a \mid 1.$$$$

Lean4

theorem not_dvd_of_one_right : FiniteMultiplicity a 1 → ¬a ∣ 1 := fun ⟨n, hn⟩ ⟨d, hd⟩ =>
  hn ⟨d ^ (n + 1), (pow_mul_pow_eq_one (n + 1) hd.symm).symm⟩

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

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

Разделы

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

Аффилиация

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