isUnit_of_finite

Mathlib.Algebra.Ring.NonZeroDivisors

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

English

If R is finite and r is right regular, then r is a unit.

Русский

Если R конечен и r является правым регулярным элементом, то r является единицей.

LaTeX

$$$$\\operatorname{IsRightRegular}(r) \\rightarrow \\operatorname{IsUnit}(r)$$$$

Lean4

theorem isUnit_of_finite (h : IsRightRegular r) : IsUnit r := by
  rwa [IsUnit.isUnit_iff_mulRight_bijective, ← Finite.injective_iff_bijective]

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

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

Разделы

Аффилиация

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