StdBasis

📁 Source: Mathlib/LinearAlgebra/Matrix/StdBasis.lean

Statistics

Metric	Count
Definitions stdBasis	1
Theorems stdBasis_eq_single, matrix_apply	2
Total	3

Matrix

Definitions

Name	Category	Theorems
stdBasis 📖	CompOp	7 math math: Module.Basis.end_repr_apply, Module.Basis.linearMap_apply, Module.Basis.end_apply, Module.Basis.linearMap_repr_apply, Module.Basis.end_repr_symm_apply, stdBasis_eq_single, Module.Basis.linearMap_repr_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
stdBasis_eq_single 📖	mathematical	—	DFunLike.coe Module.Basis Matrix addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring module Semiring.toModule Module.Basis.instFunLike stdBasis single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	RingHomInvPair.ids Module.Basis.coe_reindex Pi.basis_apply Pi.basisFun_apply single_eq_of_single_single

Module.Basis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
matrix_apply 📖	mathematical	—	DFunLike.coe Module.Basis Matrix Matrix.addCommMonoid Matrix.module instFunLike matrix Matrix.single AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	RingHomInvPair.ids coe_reindex Pi.basis_apply Matrix.single_eq_of_single_single

---

← Back to Index