inl_eq_coe_inlₗ

Mathlib.Algebra.Order.GroupWithZero.Lex

URI: https://scilib.ai/kg/mathlib#LinearOrderedCommGroupWithZero.inl_eq_coe_inlₗ

← MathLib Explorer

English

The inl map at nonzero m coincides with a canonical inlₗ map on units.

Русский

Для ненулевого m отображение inl совпадает с каноническим inlₗ на единицах.

LaTeX

$$$inl(m) = inlₗ(Units.mk0 m)$ при hm ≠ 0.$$

Lean4

theorem inl_eq_coe_inlₗ {m : α} (hm : m ≠ 0) : inl α β m = OrderMonoidHom.inlₗ αˣ βˣ (Units.mk0 _ hm) :=
  by
  lift m to αˣ using isUnit_iff_ne_zero.mpr hm
  simp

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

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

Разделы

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

Аффилиация

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