isUnit_inr_iff

Mathlib.Algebra.TrivSqZeroExt

URI: https://scilib.ai/kg/mathlib#TrivSqZeroExt.isUnit_inr_iff

← MathLib Explorer

English

IsUnit(inr(m)) is equivalent to Subsingleton R.

Русский

IsUnit(inr(m)) эквивалентно Subsingleton R.

LaTeX

$$$ IsUnit(inr(m)) \\iff Subsingleton(R) $$$

Lean4

@[simp]
theorem isUnit_inr_iff {m : M} : IsUnit (inr m : tsze R M) ↔ Subsingleton R := by
  simp_rw [isUnit_iff_isUnit_fst, fst_inr, isUnit_zero_iff, subsingleton_iff_zero_eq_one]

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

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

Разделы

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

Аффилиация

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