eq_inv_smul_iff₀

Mathlib.Algebra.GroupWithZero.Action.Units

URI: https://scilib.ai/kg/mathlib#eq_inv_smul_iff₀

English

For a ≠ 0, x = a⁻¹ • y iff a • x = y.

Русский

Для a ≠ 0, x = a⁻¹ • y тогда и только тогда, когда a • x = y.

LaTeX

$$$x = a^{-1} \\cdot y \\iff a \\cdot x = y$$$

Lean4

theorem eq_inv_smul_iff₀ (ha : a ≠ 0) {x y : β} : x = a⁻¹ • y ↔ a • x = y :=
  eq_inv_smul_iff (g := Units.mk0 a ha)

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

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

Разделы

Аффилиация

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