mul_cancel_right_coe_nonZeroDivisors

Mathlib.Algebra.Ring.NonZeroDivisors

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

English

For c ∈ R⁰, x c = y c ⇔ x = y.

Русский

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

LaTeX

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

Lean4

theorem mul_cancel_right_coe_nonZeroDivisors {c : R⁰} : x * c = y * c ↔ x = y :=
  mul_cancel_right_mem_nonZeroDivisors c.prop

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

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

Разделы

Аффилиация

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