inr_map_mul

Mathlib.LinearAlgebra.Prod

URI: https://scilib.ai/kg/mathlib#LinearMap.inr_map_mul

English

The left-inclusion map preserves multiplication: inl(a1 a2) = inl(a1) · inl(a2).

Русский

Левый инклюзив сохраняет умножение: inl(a1 a2) = inl(a1) · inl(a2).

LaTeX

$$$ \\text{inl }(a_1 a_2) = \\text{inl }(a_1) \\cdot \\text{inl }(a_2). $$$

Lean4

theorem inr_map_mul (b₁ b₂ : B) : LinearMap.inr R A B (b₁ * b₂) = LinearMap.inr R A B b₁ * LinearMap.inr R A B b₂ :=
  Prod.ext (by simp) rfl

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

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

Разделы

Аффилиация

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