star_injective

Mathlib.Algebra.Star.Basic

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

English

The star operation is injective: if star x = star y, then x = y.

Русский

Операция звезды инъективна: если star x = star y, тогда x = y.

LaTeX

$$$$ \star x = \star y \Rightarrow x = y. $$$$

Lean4

theorem star_injective [InvolutiveStar R] : Function.Injective (star : R → R) :=
  Function.Involutive.injective star_involutive

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

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

Разделы

Аффилиация

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