finsuppTensorFinsuppLid_self — Mathlib

English

The RID and the primed RID coincide, i.e., finsuppTensorFinsuppRid_self: finsuppTensorFinsuppRid R R ι κ = finsuppTensorFinsupp' R ι κ.

Русский

RID и его упрощённый RID совпадают: finsuppTensorFinsuppRid_self.

LaTeX

$$$$ \\text{finsuppTensorFinsuppRid\_self} : finsuppTensorFinsuppRid\\ R\\ R\\ ι\\ κ = finsuppTensorFinsupp'\\ R\\ ι\\ κ. $$$$

Lean4

theorem finsuppTensorFinsuppLid_self : finsuppTensorFinsuppLid R R ι κ = finsuppTensorFinsupp' R ι κ :=
  rfl

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