mk_left_injective

Mathlib.GroupTheory.MonoidLocalization.Basic

URI: https://scilib.ai/kg/mathlib#Localization.mk_left_injective

English

For a cancellative monoid, the map a ↦ mk a b is injective in a on the left.

Русский

Для мультиинвариантного моноида отображение a ↦ mk a b инъективно слева.

LaTeX

$$$\text{mk_left_injective}(b) : \text{Injective}(a \mapsto \mathrm{Localization.mk}~a~b)$$$

Lean4

@[to_additive]
theorem mk_left_injective (b : s) : Injective fun a => mk a b := fun c d h => by
  simpa [mk_eq_mk_iff, r_iff_exists] using h

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

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

Разделы

Аффилиация

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