eq_div_iff_mul_eq_of_dvd

Mathlib.Algebra.EuclideanDomain.Basic

URI: https://scilib.ai/kg/mathlib#EuclideanDomain.eq_div_iff_mul_eq_of_dvd

← MathLib Explorer

English

Let x,y,z ∈ R with y ≠ 0 and y ∣ x. Then x/y = z if and only if x = y·z.

Русский

Пусть x,y,z ∈ R, y ≠ 0 и y ∣ x. Тогда x/y = z тогда и только если x = y·z.

LaTeX

$$$$ (y \\neq 0) \\land (y \\mid x) \\Rightarrow (x/y = z \\iff x = y \\cdot z). $$$$

Lean4

theorem eq_div_iff_mul_eq_of_dvd (x y z : R) (h1 : z ≠ 0) (h2 : z ∣ y) : x = y / z ↔ z * x = y := by
  rw [eq_comm, div_eq_iff_eq_mul_of_dvd _ _ _ h1 h2, eq_comm]

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

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

Разделы

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

Аффилиация

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