transferFunction_apply — Mathlib

English

The value of transferFunction at q is exactly the explicit formula given by the left-quotient data: transferFunction(H,g,q) = g^{t(q)} · g_q, with t(q) and g_q determined by the canonical data.

Русский

Значение transferFunction в coset q задаётся явно: transferFunction(H,g,q) = g^{t(q)} · g_q, где t(q) и g_q задаются каноническими данными.

LaTeX

$$$\mathrm{transferFunction}(H,g,q) = g^{\,t(q)} \cdot g_q$$$

Lean4

theorem transferFunction_apply (q : G ⧸ H) :
    transferFunction H g q =
      g ^ (cast (quotientEquivSigmaZMod H g q).2 : ℤ) * (quotientEquivSigmaZMod H g q).1.out.out :=
  rfl

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