instMulActionQuotientDiff — Mathlib

English

If coprimality holds between |H| and index, for any two quotient representatives α, β there exists h ∈ H with h•α = β.

Русский

При условии взаимно простых порядков для H и индекса существует элемент h ∈ H, такой что h•α = β.

LaTeX

$$∃ h ∈ H, h • α = β$$

Lean4

noncomputable instance : MulAction G H.QuotientDiff
    where
  smul
    g :=
    Quotient.map' (fun α => op g⁻¹ • α) fun α β h =>
      Subtype.ext
        (by rwa [smul_diff_smul', coe_mk, coe_one, mul_eq_one_iff_eq_inv, mul_eq_left, ← coe_one, ← Subtype.ext_iff])
  mul_smul g₁ g₂
    q :=
    Quotient.inductionOn' q fun T => congr_arg Quotient.mk'' (by rw [mul_inv_rev]; exact mul_smul (op g₁⁻¹) (op g₂⁻¹) T)
  one_smul q := Quotient.inductionOn' q fun T => congr_arg Quotient.mk'' (by rw [inv_one]; apply one_smul Gᵐᵒᵖ T)

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