floorRoot_one_right

Mathlib.Data.Nat.Factorization.Root

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

English

If n ≠ 0, then floorRoot(n,1) = 1.

Русский

Если n ≠ 0, то floorRoot(n,1) = 1.

LaTeX

$$$\forall n\,(n \neq 0) \Rightarrow \text{floorRoot}(n,1)=1$$$

Lean4

@[simp]
theorem floorRoot_one_right (hn : n ≠ 0) : floorRoot n 1 = 1 := by simp [floorRoot, hn]

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

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

Разделы

Аффилиация

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