restrictScalars_coe_coroot — Mathlib

English

Under the same base-change as above, the coroots are preserved; restricting scalars does not alter the coroot associated to any index i.

Русский

При том же изменении базы короты сохраняются; ограничение скаляров не изменяет короот, ассоциированный с индексом i.

LaTeX

$$$\\forall i \\ (P.restrictScalars' K hP).coroot(i) = P.coroot(i)$$$

Lean4

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

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