isUnit_iff_eq_one

Mathlib.Algebra.Group.Units.Defs

URI: https://scilib.ai/kg/mathlib#isUnit_iff_eq_one

← MathLib Explorer

English

Under a subsingleton of units, IsUnit x is equivalent to x = 1.

Русский

При условии подединицы единиц, IsUnit x эквивалентно x = 1.

LaTeX

$$IsUnit(x) \iff x = 1$$

Lean4

@[to_additive (attr := simp)]
theorem isUnit_iff_eq_one [Subsingleton Mˣ] {x : M} : IsUnit x ↔ x = 1 :=
  ⟨fun ⟨u, hu⟩ ↦ by rw [← hu, Subsingleton.elim u 1, Units.val_one], fun h ↦ h ▸ isUnit_one⟩

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

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

Разделы

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

Аффилиация

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