mul_left_eq_self_iff

Mathlib.Algebra.Regular.Basic

URI: https://scilib.ai/kg/mathlib#IsLeftRegular.mul_left_eq_self_iff

← MathLib Explorer

English

If IsLeftRegular a, then a*b = a iff b = 1.

Русский

Если IsLeftRegular a, то a*b = a эквивалентно b = 1.

LaTeX

$$$ IsLeftRegular a \rightarrow (a * b = a \leftrightarrow b = 1) $$$

Lean4

@[to_additive (attr := simp)]
theorem mul_left_eq_self_iff (ha : IsLeftRegular a) : a * b = a ↔ b = 1 :=
  ⟨fun h ↦ by rwa [← ha.eq_iff, mul_one], fun h ↦ by rw [h, mul_one]⟩

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

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

Разделы

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

Аффилиация

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