mulMapLeftOfSupEqTop_tmul

Mathlib.RingTheory.LinearDisjoint

URI: https://scilib.ai/kg/mathlib#Subalgebra.LinearDisjoint.mulMapLeftOfSupEqTop_tmul

English

In the same setting, the image of a ⊗ b under mulMapLeftOfSupEqTop is a·b in S.

Русский

При тех же условиях образ a ⊗ b под mulMapLeftOfSupEqTop равен a·b в S.

LaTeX

$$$H.mulMapLeftOfSupEqTop H' (a \\otimes_R b) = a \\cdot b$$$

Lean4

@[simp]
theorem mulMapLeftOfSupEqTop_tmul (H' : A ⊔ B = ⊤) (a : A) (b : B) :
    H.mulMapLeftOfSupEqTop H' (a ⊗ₜ[R] b) = (a : S) * (b : S) :=
  rfl

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

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

Разделы

Аффилиация

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