inr_eq_coe_inrₗ

Mathlib.Algebra.Order.GroupWithZero.Lex

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

← MathLib Explorer

English

The inr map at a nonzero element equals the canonical inrₗ on units.

Русский

inr на ненулевом элементе равен каноническому inrℓ на единицах.

LaTeX

$$$inr(n) = inrₗ(Units.mk0 n)$ при hn ≠ 0.$$

Lean4

theorem inr_eq_coe_inrₗ {n : β} (hn : n ≠ 0) : inr α β n = OrderMonoidHom.inrₗ αˣ βˣ (Units.mk0 _ hn) :=
  by
  lift n to βˣ using isUnit_iff_ne_zero.mpr hn
  simp

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

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

Разделы

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

Аффилиация

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