divp_eq_iff_mul_eq

Mathlib.Algebra.Group.Units.Basic

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

← MathLib Explorer

English

For any x, unit u, y, x /ₚ u = y iff y·u = x.

Русский

Для любых x, единицы u и y, x /ₚ u = y тогда и только тогда y·u = x.

LaTeX

$$$\forall x\in \alpha, \; u\in \alpha^{\times}, \; y\in \alpha:\; x /ₚ u = y \iff y\,u = x$$$

Lean4

theorem divp_eq_iff_mul_eq {x : α} {u : αˣ} {y : α} : x /ₚ u = y ↔ y * u = x :=
  u.mul_left_inj.symm.trans <| by rw [divp_mul_cancel]; exact ⟨Eq.symm, Eq.symm⟩

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

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

Разделы

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

Аффилиация

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