rotation_injective

Mathlib.Analysis.Complex.Isometry

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

English

The map rotation is injective: if rotation a = rotation b, then a = b.

Русский

Отображение rotation текуще инъективно: если rotation a = rotation b, то a = b.

LaTeX

$$Inj: rotation is injective$$

Lean4

theorem rotation_injective : Function.Injective rotation :=
  Function.LeftInverse.injective rotationOf_rotation

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

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

Разделы

Аффилиация

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