sqrt_eq_one_iff' — Mathlib

English

For a suitably structured algebra A, the equality sqrt(a) = 1 is equivalent to a = 1 (assuming A is nontrivial).

Русский

Для надлежащей структуры алгебры A равенство sqrt(a) = 1 эквивалентно a = 1 (при условии, что A ненулевая).

LaTeX

$$$\sqrt{a} = 1 \iff a = 1$$$

Lean4

theorem sqrt_eq_one_iff' [Nontrivial A] (a : A) : sqrt a = 1 ↔ a = 1 :=
  by
  refine ⟨fun h ↦ sqrt_eq_one_iff a ?_ |>.mp h, fun h ↦ h ▸ sqrt_one⟩
  rw [sqrt, cfcₙ] at h
  cfc_tac
    -- TODO: relate to a strict positivity condition

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