toLin_eq_toLin' — Mathlib

English

For the standard bases, the mapping Matrix.toLin coincides with the general toLin; i.e., Matrix.toLin (Pi.basisFun R n) (Pi.basisFun R m) = Matrix.toLin'.

Русский

Для стандартных базисов отображение Matrix.toLin совпадает с общим toLin; то есть Matrix.toLin (Pi.basisFun R n) (Pi.basisFun R m) = Matrix.toLin'.

LaTeX

$$$\\text{toLin}_{\\mathrm{std}} = \\text{toLin}'. $$$

Lean4

/-- `Matrix.toLin'` is a particular case of `Matrix.toLin`, for the standard basis
`Pi.basisFun R n`. -/
theorem toLin_eq_toLin' : Matrix.toLin (Pi.basisFun R n) (Pi.basisFun R m) = Matrix.toLin' :=
  rfl

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