comp_symm_eq — Mathlib

English

Let e be a monoid isomorphism M ≃* N, f: N → α, g: M → α. Then g ∘ e^{-1} = f if and only if g = f ∘ e.

Русский

Пусть e — изоморфизм моидов M ≃* N, f: N → α, g: M → α. Тогда g ∘ e^{-1} = f эквивалентно g = f ∘ e.

LaTeX

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

Lean4

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

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