dimension_reindex — Mathlib

English

Reindexing a presentation by Equivalences e and f leaves its dimension unchanged.

Русский

Переиндексация презентации по эквивалентностям e и f не изменяет размерности.

LaTeX

$$$\\mathrm{dimension\\_reindex}(P,e,f) = \\mathrm{dimension}(P)$$$

Lean4

@[simp]
theorem dimension_reindex (P : Presentation R S ι σ) {ι' σ' : Type*} (e : ι' ≃ ι) (f : σ' ≃ σ) :
    (P.reindex e f).dimension = P.dimension := by simp [dimension, Nat.card_congr e, Nat.card_congr f]

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