reindexₐ_symm — Mathlib

English

For finite index sets m, n and a bijection e: m ≃ n, reindexₐ R A e.symm = (reindexₐ R A e).symm.

Русский

Для конечных множеств индексов m, n и биекции e: m ≃ n выполняется reindexₐ R A e.symm = (reindexₐ R A e).symm.

LaTeX

$$$$ \\mathrm{reindex}_A R A e^{-1} = (\\mathrm{reindex}_A R A e)^{-1} $$$$

Lean4

@[simp]
theorem reindexₐ_symm [Fintype m] [Fintype n] [Semiring R] [AddCommMonoid A] [Mul A] [Module R A] [Star A] {e : m ≃ n} :
    reindexₐ R A e.symm = (reindexₐ R A e).symm := by simp [reindexₐ, reindexₗ]

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