prod_repr_inl — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem prod_repr_inl (x) (i) : (b.prod b').repr x (Sum.inl i) = b.repr x.1 i :=
  rfl

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