isUnit_of_finite

Mathlib.Algebra.Ring.NonZeroDivisors

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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