Basis — Mathlib

English

There is a free ℤ-module structure on LocallyConstant S ℤ given a suitable isomorphism with GoodProducts.

Русский

Существует свободная структура модуля над целыми числами на LocallyConstant S ℤ, заданная подходящим изоморфизмом с GoodProducts.

LaTeX

$$$\\text{Nobeling_aux } :\\; \\text{Module.Free }\\mathbb{Z}(\\ LocallyConstant S\\mathbb{Z}).$$$

Lean4

/-- `GoodProducts C` as a `ℤ`-basis for `LocallyConstant C ℤ`. -/
noncomputable def Basis (hC : IsClosed C) : Basis (GoodProducts C) ℤ (LocallyConstant C ℤ) :=
  Basis.mk (GoodProducts.linearIndependent C hC) (GoodProducts.span C hC)

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