eq_comp_symm — Mathlib

English

Let e be a monoid isomorphism M ≃* N and f: N → α, g: M → α. Then f equals g composed with the inverse of e if and only if f composed with e equals g.

Русский

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

LaTeX

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

Lean4

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

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