coe_eq_one — Mathlib

English

For a in the closed unit ball, a equals 1 in 𝕜 if and only if a equals 1 in the ball.

Русский

Для элемента a из замкнутого шара единицы верно: a в 𝕜 равно 1 тогда и только тогда, когда a = 1 в шаре.

LaTeX

$$$(a : 𝕜) = 1 \iff a = 1$$$

Lean4

@[simp, norm_cast]
protected theorem coe_eq_one [SeminormedRing 𝕜] [NormOneClass 𝕜] {a : closedBall (0 : 𝕜) 1} : (a : 𝕜) = 1 ↔ a = 1 :=
  Subtype.val_injective.eq_iff' unitClosedBall.coe_one

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