restrictScalars_coe_root — Mathlib

English

Let P be a root pairing with a suitable balanced structure. For any base-change from L to K with a compatible map, the root indices are preserved under restriction of scalars: for every i, the root index remains the same after restricting scalars.

Русский

Пусть P — корневая паринговая структура с подходящей балансировкой. При любом изменении базы из L в K с совместимой связью корнями сохраняется соответствие индексов корня: для каждого i корень i сохраняется после ограничения скаляров.

LaTeX

$$$\\forall i \\in \\iota: \\ (P.restrictScalars' K hP).root(i) = P.root(i)$$$

Lean4

@[simp]
theorem restrictScalars_coe_root (i : ι) : (P.restrictScalars' K hP).root i = P.root i :=
  rfl

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