freeMonoidCongr_symm_of — Mathlib

English

Let e: α ≃ β be a bijection and let b ∈ β. Then the image of the generator corresponding to b under the inverse induced map on the free monoid equals the generator corresponding to e.symm b. In symbols, freeMonoidCongr e.symm (of b) = of (e.symm b).

Русский

Пусть e: α ≃ β — биекция и b ∈ β. Тогда образ порождающего b под индуцированного отображения свободного моноида по обратному эквиваленту e равен порождающему e.symm b: freeMonoidCongr e.symm (of b) = of (e.symm b).

LaTeX

$$$\\mathrm{freeMonoidCongr}(e^{\\mathrm{symm}})(\\mathrm{of}(b)) = \\mathrm{of}(e^{\\mathrm{symm}}(b)).$$$

Lean4

@[to_additive (attr := simp)]
theorem freeMonoidCongr_symm_of (e : α ≃ β) (b : β) : freeMonoidCongr e.symm (of b) = of (e.symm b) :=
  rfl

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