neZero_totient

Mathlib.Data.Nat.Totient

URI: https://scilib.ai/kg/mathlib#Nat.neZero_totient

English

Basic positivity relations; see totient_pos for details.

Русский

Базовые соотношения положительности; смотрите totient_pos.

LaTeX

$$$$\text{see totient_pos}.$$$$

Lean4

instance neZero_totient {n : ℕ} [NeZero n] : NeZero n.totient :=
  ⟨(totient_pos.mpr <| NeZero.pos n).ne'⟩

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

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

Разделы

Аффилиация

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