mul_comp

Mathlib.Algebra.Order.Hom.MonoidWithZero

URI: https://scilib.ai/kg/mathlib#OrderMonoidWithZeroHom.mul_comp

English

If hf is surjective, then (g1.comp f) = (g2.comp f) implies g1=g2.

Русский

Если hf сюръективно, то (g1 ∘ f) = (g2 ∘ f) => g1=g2.

LaTeX

$$$(g_1 \circ f) = (g_2 \circ f) \Rightarrow g_1 = g_2 \quad(\text{при } hf \text{ сюръективности})$$$

Lean4

theorem mul_comp (g₁ g₂ : β →*₀o γ) (f : α →*₀o β) : (g₁ * g₂).comp f = g₁.comp f * g₂.comp f :=
  rfl

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

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

Разделы

Аффилиация

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