algebraMap_coxeterWeightIn — Mathlib

English

Algebra map carries Coxeter weights from the valued-in-set S to R unchanged.

Русский

Алгебраическая карта сохраняет Coxeter weights при переходе из S в R.

LaTeX

$$algebraMap S R (P.coxeterWeightIn S i j) = P.coxeterWeight i j$$

Lean4

@[simp]
theorem algebraMap_coxeterWeightIn (S : Type*) [CommRing S] [Algebra S R] [P.IsValuedIn S] (i j : ι) :
    algebraMap S R (P.coxeterWeightIn S i j) = P.coxeterWeight i j := by simp [coxeterWeightIn, coxeterWeight]

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