sign_kerParam_apply_apply — Mathlib

English

The injection property of kerParam is established; two different inputs give different permutations.

Русский

Свойство инъективности kerParam доказано; разные входы дают разные перестановки.

LaTeX

$$kerParam_injective$$

Lean4

theorem sign_kerParam_apply_apply : sign (kerParam g ⟨k, v⟩) = sign k * ∏ c, sign (v c).val :=
  by
  rw [kerParam, MonoidHom.noncommCoprod_apply, ← Prod.fst_mul_snd ⟨k, v⟩, Prod.mk_mul_mk, mul_one, one_mul, map_mul,
    sign_ofSubtype, Finset.univ_eq_attach, mul_right_inj, ← MonoidHom.comp_apply, Subgroup.noncommPiCoprod,
    MonoidHom.comp_noncommPiCoprod _, MonoidHom.noncommPiCoprod_apply, Finset.univ_eq_attach,
    Finset.noncommProd_eq_prod]
  simp

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