inl_mul_inl

Mathlib.Algebra.Algebra.Unitization

URI: https://scilib.ai/kg/mathlib#Unitization.inl_mul_inl

← MathLib Explorer

English

For r1, r2 ∈ R, inl(r1) · inl(r2) = inl(r1 r2).

Русский

Для r1, r2 ∈ R: inl(r1) · inl(r2) = inl(r1 r2).

LaTeX

$$$\mathrm{inl}(r_1) \cdot \mathrm{inl}(r_2) = \mathrm{inl}(r_1 r_2).$$$

Lean4

theorem inl_mul_inl [Mul R] [NonUnitalNonAssocSemiring A] [SMulZeroClass R A] (r₁ r₂ : R) :
    (inl r₁ * inl r₂ : Unitization R A) = inl (r₁ * r₂) :=
  (inl_mul A r₁ r₂).symm

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

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

Разделы

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

Аффилиация

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