coord_apply_embedding_eq_smul_coord

English

Applying coordinates after embedding corresponds to smul by a on the corresponding coordinates of the basis for N.

Русский

Применение координат после вложения соответствует умножению на a на соответствующие координаты базы N.

LaTeX

$$$snf.bM.coord (snf.f i) \\circ_N.subtype = (snf.a i) · snf.bN.coord i$$$

Lean4

@[simp]
theorem coord_apply_embedding_eq_smul_coord {i : Fin n} :
    snf.bM.coord (snf.f i) ∘ₗ N.subtype = snf.a i • snf.bN.coord i :=
  by
  ext m
  simp [Pi.smul_apply (snf.a i)]

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