to_isCancelMulZero

Mathlib.Algebra.GroupWithZero.Defs

URI: https://scilib.ai/kg/mathlib#IsRightCancelMulZero.to_isCancelMulZero

English

If a right-cancellation property holds, then IsCancelMulZero follows.

Русский

Если выполняется правое отменение, следует свойство отмены по нулю.

LaTeX

$$$\text{IsRightCancelMulZero}(M_0) \Rightarrow \text{IsCancelMulZero}(M_0)$$$

Lean4

theorem to_isCancelMulZero [IsRightCancelMulZero M₀] : IsCancelMulZero M₀ :=
  { IsRightCancelMulZero.to_isLeftCancelMulZero with }

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

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

Разделы

Аффилиация

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