mul_right_eq_self_iff

Mathlib.Algebra.Regular.Basic

URI: https://scilib.ai/kg/mathlib#IsRightRegular.mul_right_eq_self_iff

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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