dvd_cancel_left

Mathlib.Algebra.Divisibility.Basic

URI: https://scilib.ai/kg/mathlib#IsLeftRegular.dvd_cancel_left

← MathLib Explorer

English

If a is left regular, then a·b | a·c iff b | c.

Русский

Если a-для слева регулярна, тогда a·b | a·c тогда и только если b | c.

LaTeX

$$$$\text{If }a\text{ is left regular }a b\mid a c \iff b\mid c.$$$$

Lean4

theorem dvd_cancel_left (h : IsLeftRegular a) : a * b ∣ a * c ↔ b ∣ c :=
  ⟨fun dvd ↦
    have ⟨d, eq⟩ := dvd;
    ⟨d, h (eq.trans <| mul_assoc ..)⟩,
    mul_dvd_mul_left a⟩

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

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

Разделы

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

Аффилиация

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