cartanMatrixIn_apply_same — Mathlib

English

There exists a canonical equivalence on the index set ι induced by mapsTo-preserving reflections; this equivalence respects the root data.

Русский

Существует каноническое эквивалентное отображение на множестве индексов ι, индуцируемое отражениями, сохраняющими пары корней; эквивалентность сохраняет данные корней.

LaTeX

$$$\\text{equiv\_of\_mapsTo} : ι \\simeq ι$ (bijective and compatible with roots/coroots)$$

Lean4

@[simp]
theorem cartanMatrixIn_apply_same [FaithfulSMul S R] (i : b.support) : b.cartanMatrixIn S i i = 2 :=
  FaithfulSMul.algebraMap_injective S R <| by
    simp [cartanMatrixIn_def, map_ofNat]
      /- If we generalised the notion of `RootPairing.Base` to work relative to an assumption
      `[P.IsValuedIn S]` then such a base would provide basis of `P.rootSpan S` and we could avoid
      using `Matrix.map` below. -/

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