singleton — Mathlib

English

Basis.singleton ι R is the basis sending the unique element of ι to 1 ∈ R.

Русский

Basis.singleton ι R — базис, отправляющий единственный элемент ι в 1 ∈ R.

LaTeX

$$Protected definition: Basis.singleton ι R$$

Lean4

/-- `Basis.singleton ι R` is the basis sending the unique element of `ι` to `1 : R`. -/
protected def singleton (ι R : Type*) [Unique ι] [Semiring R] : Basis ι R R :=
  ofRepr
    { toFun := fun x => Finsupp.single default x
      invFun := fun f => f default
      left_inv := fun x => by simp
      right_inv := fun f => Finsupp.unique_ext (by simp)
      map_add' := fun x y => by simp
      map_smul' := fun c x => by simp }

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