smul_eq_map — Mathlib

English

The representation of g • b is obtained by composing b.repr with the inverse of the action linear equivalence: (g • b).repr = (DistribMulAction.toLinearEquiv _ _ g).symm.trans b.repr.

Русский

Представление g • b получается как композиция представления b с обратным линейным отображением действия: (g • b).repr = (DistribMulAction.toLinearEquiv _ _ g).symm.trans b.repr.

LaTeX

$$(g \cdot b).repr = (\mathrm{DistribMulAction.toLinearEquiv} _ _ g).symm.\trans b.repr$$

Lean4

/-- When the group in question is the automorphisms, `•` coincides with `Basis.map`. -/
@[simp]
theorem smul_eq_map (g : M ≃ₗ[R] M) (b : Basis ι R M) : g • b = b.map g :=
  rfl

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