coe_transferFunction — Mathlib

English

The coset of transferFunction(H,g,q) is exactly q; i.e., transferFunction selects a representative of q whose image in G/H is q.

Русский

Косет transferFunction(H,g,q) в G/H равен q; то есть transferFunction выбирает представитель косета, образ которого в G/H равен q.

LaTeX

$$$\pi\bigl(\mathrm{transferFunction}(H,g,q)\bigr) = q$$$

Lean4

theorem coe_transferFunction (q : G ⧸ H) : ↑(transferFunction H g q) = q := by
  rw [transferFunction_apply, ← smul_eq_mul, Quotient.coe_smul_out, ← quotientEquivSigmaZMod_symm_apply, Sigma.eta,
    symm_apply_apply]

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