viaFintypeEmbedding_sign — Mathlib

English

The sign is preserved when passing to a finite-type embedding of the domain.

Русский

Знак сохраняется при переходе к отображению через вложение в конечный тип.

LaTeX

$$$\\operatorname{sign}(\\mathrm{viaFintypeEmbedding}(e,f)) = \\operatorname{sign}(e)$$$

Lean4

@[simp]
theorem viaFintypeEmbedding_sign [Fintype α] [Fintype β] [DecidableEq β] (e : Equiv.Perm α) (f : α ↪ β) :
    sign (e.viaFintypeEmbedding f) = sign e := by simp [viaFintypeEmbedding]

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