ceilRoot_ne_zero

Mathlib.Data.Nat.Factorization.Root

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

English

The nonzeroness of ceilRoot n a is equivalent to n ≠ 0 and a ≠ 0.

Русский

Ненулевой ceilRoot n a эквивалентен n ≠ 0 и a ≠ 0.

LaTeX

$$$ \operatorname{ceilRoot}(n,a) \neq 0 \iff n \neq 0 \land a \neq 0 $$$

Lean4

theorem ceilRoot_ne_zero : ceilRoot n a ≠ 0 ↔ n ≠ 0 ∧ a ≠ 0 := by simp +contextual [ceilRoot_def, not_or]

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

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

Разделы

Аффилиация

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