symm_comp_eq

Mathlib.Algebra.Group.Equiv.Defs

URI: https://scilib.ai/kg/mathlib#MulEquiv.symm_comp_eq

English

Similarly, e^{-1} ∘ g = f iff g = e ∘ f.

Русский

Аналогично, e^{-1} ∘ g = f эквивалентно g = e ∘ f.

LaTeX

$$$$ e^{-1} \circ g = f \;\iff\; g = e \circ f. $$$$

Lean4

@[to_additive]
theorem symm_comp_eq {α : Type*} (e : M ≃* N) (f : α → M) (g : α → N) : e.symm ∘ g = f ↔ g = e ∘ f :=
  e.toEquiv.symm_comp_eq f g

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

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

Разделы

Аффилиация

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