normedRing — Mathlib

English

The distance in the subalgebra equals the ambient distance of the difference: dist_S(x,y) = ∥x−y∥.

Русский

Расстояние внутри подпалгебры равно расстоянию в окружающем кольце между разности x−y.

LaTeX

$$$\forall x,y \in S:\ dist_S(x,y) = \|x-y\|_E.$$$

Lean4

/-- A subalgebra of a normed ring is also a normed ring, with the restriction of the
norm. -/
instance (priority := 75) normedRing {S 𝕜 E : Type*} [CommRing 𝕜] [NormedRing E] [Algebra 𝕜 E] [SetLike S E]
    [SubringClass S E] [SMulMemClass S 𝕜 E] (s : S) : NormedRing s :=
  { seminormedRing s with eq_of_dist_eq_zero := eq_of_dist_eq_zero }

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