mul_cancel_left_coe_nonZeroDivisors

Mathlib.Algebra.Ring.NonZeroDivisors

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

English

For c ∈ R⁰, (c : R) x = c y ⇔ x = y.

Русский

Для c ∈ R⁰, (c : R) x = c y ⇔ x = y.

LaTeX

$$$${c : R^{0}}: (c : R) \\cdot x = c \\cdot y \\iff x = y$$$$

Lean4

theorem mul_cancel_left_coe_nonZeroDivisors {c : R⁰} : (c : R) * x = c * y ↔ x = y :=
  mul_cancel_left_mem_nonZeroDivisors c.prop

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

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

Разделы

Аффилиация

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