mulLECancellable_one

Mathlib.Algebra.Order.Monoid.Unbundled.Basic

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

← MathLib Explorer

English

Left-cancellation by the unit element holds in any Monoid with order: 1 · x = x.

Русский

Левая отменяемость единицы в моноиде с порядком: 1 · x = x.

LaTeX

$$$MulLECancellable(1)$$$

Lean4

@[to_additive (attr := simp)]
theorem mulLECancellable_one [MulOneClass α] [LE α] : MulLECancellable (1 : α) := fun a b => by
  simpa only [one_mul] using id

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

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

Разделы

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

Аффилиация

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