smul_eq_iff_eq_invOf_smul

Mathlib.Algebra.Group.Action.Basic

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

English

c • x = y iff x = ⅟c • y, using the unit of invertible c.

Русский

c • x = y эквивалентно x = ⅟c • y, через единицу invertible c.

LaTeX

$$$ c \cdot x = y \iff x = ⅟c \cdot y $$$

Lean4

theorem smul_eq_iff_eq_invOf_smul : c • x = y ↔ x = ⅟c • y :=
  smul_eq_iff_eq_inv_smul (g := unitOfInvertible c)

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

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

Разделы

Аффилиация

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