coe_inj

Mathlib.GroupTheory.DivisibleHull

URI: https://scilib.ai/kg/mathlib#DivisibleHull.coe_inj

English

The coercion from M into DivisibleHull M is injective; equivalently, (m in DivisibleHull M) = (m' in DivisibleHull M) implies m = m'.

Русский

Коэрция из $M$ в $DivisibleHull M$ инъективна; то есть $(m)=(m')$ в оболочке $\iff m=m'$.

LaTeX

$$$$ (m) = (m') \\iff m = m'. $$$$

Lean4

@[simp, norm_cast]
theorem coe_inj {m m' : M} : (m : DivisibleHull M) = ↑m' ↔ m = m' :=
  coe_injective.eq_iff

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

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

Разделы

Аффилиация

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