range_equiv_smaller_toFun — Mathlib

English

A linear independence equivalence between GoodProducts eval and smaller is established via a factorization.

Русский

Установлено эквивалентность линейной независимости для GoodProducts eval и smaller через факторизацию.

LaTeX

$$$$\\text{LinearIndependent}_{\\mathbb{Z}}\\big(\\mathrm{GoodProducts}.\\mathrm{eval}(\\pi C (ord\\; I ·< o))\\big) \\Leftrightarrow \\text{LinearIndependent}_{\\mathbb{Z}}\\big( p \\mapsto p.1 \\big)$$$$

Lean4

/-- The map from the image of the `GoodProducts` in `LocallyConstant (π C (ord I · < o)) ℤ` to
`smaller C o`
-/
noncomputable def range_equiv_smaller_toFun (o : Ordinal) (x : range (π C (ord I · < o))) : smaller C o :=
  ⟨πs C o ↑x, x.val, x.property, rfl⟩

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