repr_apply_coe — Mathlib

English

For a free group basis b and an index i, the representation maps the i-th generator to the canonical generator FreeGroup.of i.

Русский

Для базы свобдной группы b и индекса i отображение представления отправляет i-й генератор в стандартный генератор FreeGroup.of i.

LaTeX

$$$$ b.repr(b i) = \\mathrm{FreeGroup.of}(i). $$$$

Lean4

@[simp]
theorem repr_apply_coe (b : FreeGroupBasis ι G) (i : ι) : b.repr (b i) = FreeGroup.of i :=
  by
  change b.repr (b.repr.symm (FreeGroup.of i)) = FreeGroup.of i
  simp

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