divp_left_inj

Mathlib.Algebra.Group.Units.Basic

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

English

Division by a unit on the left is injective: a /ₚ u = b /ₚ u iff a = b.

Русский

Деление слева на единицу инъективно: a /ₚ u = b /ₚ u эквивалентно a = b.

LaTeX

$$$\forall a,b\in \alpha:\; a /ₚ u = b /ₚ u \iff a = b$$$

Lean4

@[simp]
theorem divp_left_inj (u : αˣ) {a b : α} : a /ₚ u = b /ₚ u ↔ a = b :=
  Units.mul_left_inj _

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

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

Разделы

Аффилиация

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