fintypeOfFintype — Mathlib

English

The inverse of the basis equivalence sent to the function is the sum of scalar multiples of basis vectors: b.equivFun.symm x = ∑ i, x i • b_i.

Русский

Обратное к базисной эквивалентности отображает x в сумму координат: b.equivFun.symm x = ∑_i x_i • b_i.

LaTeX

$$$b.\equivFun^{−1}(x) = \sum_i x(i) \, b_i$$$

Lean4

/-- A module over a finite ring that admits a finite basis is finite. -/
def fintypeOfFintype [Fintype ι] (b : Basis ι R M) [Fintype R] : Fintype M :=
  haveI := Classical.decEq ι
  Fintype.ofEquiv _ b.equivFun.toEquiv.symm

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