unitsCenterToCenterUnits_injective

Mathlib.GroupTheory.Submonoid.Center

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

← MathLib Explorer

English

If two unit images coincide, then the original units are equal.

Русский

Если образы двух единиц совпадают, то сами единицы равны.

LaTeX

$$inj(unitsCenterToCenterUnits M)$$

Lean4

@[to_additive]
theorem unitsCenterToCenterUnits_injective [Monoid M] : Function.Injective (unitsCenterToCenterUnits M) :=
  fun _a _b h => Units.ext <| Subtype.ext <| congr_arg (Units.val ∘ Subtype.val) h

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

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

Разделы

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

Аффилиация

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