repr_unitsSMul — Mathlib

English

For e a basis over R2 and w a map to units, the i-th coordinate of the representation of v under e.unitsSMul equals (w i)^{-1} times the i-th coordinate of the representation of v under e.

Русский

Для e — базисa над R2 и w:ι → Units R2, i-я координата представления v под e.unitsSMul равна (w i)^{-1} умножить на i-ю координату представления v под e.

LaTeX

$$(e.unitsSMul w).repr v i = (w i)^{-1} \cdot e.repr v i$$

Lean4

@[simp]
theorem repr_unitsSMul (e : Basis ι R₂ M) (w : ι → R₂ˣ) (v : M) (i : ι) :
    (e.unitsSMul w).repr v i = (w i)⁻¹ • e.repr v i :=
  congr_arg (fun f : M →ₗ[R₂] R₂ => f v) (e.coord_unitsSMul w i)

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