sqrt_one — Mathlib

English

In any suitable algebra with the stated functional calculus structure, the principal square root of the unit element is the unit itself: sqrt(1) = 1.

Русский

В подходящей алгебре с указанной функциональной калькуляцией квадратный корень от единицы равен единице: sqrt(1) = 1.

LaTeX

$$$\sqrt{1} = 1$$$

Lean4

@[simp]
theorem sqrt_one : sqrt (1 : A) = 1 := by simp [sqrt_eq_cfc]

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