mul_cancel_left_mem_nonZeroDivisorsLeft

Mathlib.Algebra.Ring.NonZeroDivisors

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

← MathLib Explorer

English

If r ∈ nonZeroDivisorsLeft R, then r x = r y iff x = y.

Русский

Если r ∈ nonZeroDivisorsLeft R, то r x = r y эквивалентно x = y.

LaTeX

$$$$r \\in \\text{nonZeroDivisorsLeft } R \\Rightarrow (r x = r y \\iff x = y)$$$$

Lean4

theorem mul_cancel_left_mem_nonZeroDivisorsLeft (hr : r ∈ nonZeroDivisorsLeft R) : r * x = r * y ↔ x = y :=
  ⟨(isLeftRegular_iff_mem_nonZeroDivisorsLeft.mpr hr ·), congr_arg (r * ·)⟩

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

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

Разделы

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

Аффилиация

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