coe_parallelepiped — Mathlib

English

The parallelepiped of a basis equals the parallelepiped defined by its coordinate representation.

Русский

Параллелепипед базиса равен параллелепипеду, заданному его координатным представлением.

LaTeX

$$$ (b.parallelepiped : Set E) = parallelepiped (b.coe) $.$$

Lean4

@[simp]
theorem coe_parallelepiped (b : Basis ι ℝ E) : (b.parallelepiped : Set E) = _root_.parallelepiped b :=
  rfl

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