eq_symm_comp

Mathlib.Algebra.Group.Equiv.Defs

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

English

For e ∈ MulEquiv M N, f: α → M and g: α → N, f = e.symm ∘ g if and only if e ∘ f = g.

Русский

Для e ∈ MulEquiv M N, f: α → M и g: α → N, равенство f = e^{-1} ∘ g эквивалентно g = e ∘ f.

LaTeX

$$$$ f = e.symm \circ g \;\iff\; e \circ f = g. $$$$

Lean4

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

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

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

Разделы

Аффилиация

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