prod_repr_inr — Mathlib

English

For all x in M × M' and i in ι', the i-th coordinate of the representation of x with respect to the product equals the i-th coordinate of the representation of the second component with respect to b'.

Русский

Пусть x = (x1, x2). Координата i справа в представлении базиса b.prod b' равна координате i в представлении x2 базисом b'.

LaTeX

$$$(b.prod b').repr x (\mathrm{Sum.inr} i) = b'.repr x_2 i$$$

Lean4

@[simp]
theorem prod_repr_inr (x) (i) : (b.prod b').repr x (Sum.inr i) = b'.repr x.2 i :=
  rfl

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