dist_mul_self_right

Mathlib.Analysis.Normed.Group.Uniform

URI: https://scilib.ai/kg/mathlib#dist_mul_self_right

← MathLib Explorer

English

In a normed group, the distance from b to a⋅b equals the norm of a.

Русский

В нормированной группе расстояние между b и a⋅b равно норме элемента a.

LaTeX

$$$\\operatorname{dist}(b, a\\cdot b) = \\|a\\|$$$

Lean4

@[to_additive (attr := simp)]
theorem dist_mul_self_right (a b : E) : dist b (a * b) = ‖a‖ := by rw [← dist_one_left, ← dist_mul_right 1 a b, one_mul]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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