StdBasis

📁 Source: Mathlib/LinearAlgebra/StdBasis.lean

Statistics

Metric	Count
Definitions piEquiv, basis, basisFun	3
Theorems eq_piEvalAlgHom, function, pi, piEquiv_apply_apply, range_piEquiv, surjective_piEquiv_apply_iff, basisFun_apply, basisFun_equivFun, basisFun_repr, basis_apply, basis_repr, basis_repr_single, linearIndependent_single, linearIndependent_single_of_ne_zero, linearIndependent_single_one	15
Total	18

AlgHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_piEvalAlgHom 📖	mathematical	—	Pi.evalAlgHom CommSemiring.toSemiring Algebra.id	—	map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass algHomClass Finset.sum_congr Finset.sum_const_zero NeZero.one Finset.univ_sum_single map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass AlgHomClass.linearMapClass NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass Pi.single_eq_same Pi.single_eq_of_ne' MulZeroClass.mul_zero Pi.single_eq_of_ne MulZeroClass.zero_mul map_zero MonoidWithZeroHomClass.toZeroHomClass Fintype.sum_eq_single toLinearMap_injective Module.Basis.ext Pi.basisFun_apply

Module

Definitions

Name	Category	Theorems
piEquiv 📖	CompOp	3 math math: piEquiv_apply_apply, range_piEquiv, surjective_piEquiv_apply_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
piEquiv_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike LinearEquiv RingHomInvPair.ids LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv piEquiv Finite.of_fintype Finset.sum Finset.univ SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype Basis.constr_apply_fintype Finset.sum_congr
range_piEquiv 📖	mathematical	—	LinearMap.range CommSemiring.toSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule RingHom.id RingHomSurjective.ids DFunLike.coe LinearEquiv RingHomInvPair.ids LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv piEquiv Submodule.span Set.range	—	Basis.constr_range
surjective_piEquiv_apply_iff 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike LinearEquiv RingHomInvPair.ids LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv piEquiv Submodule.span Set.range Top.top Submodule Submodule.instTop	—	RingHomInvPair.ids smulCommClass_self RingHomSurjective.ids LinearMap.range_eq_top range_piEquiv

Module.Free

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
function 📖	mathematical	—	Module.Free Pi.addCommMonoid Pi.Function.module	—	pi
pi 📖	mathematical	Module.Free	Pi.addCommMonoid Pi.module	—	nonempty_fintype of_basis

Pi

Definitions

Name	Category	Theorems
basis 📖	CompOp	4 math math: basis_repr_single, basis_apply, basis_repr, orthonormalBasis.toBasis
basisFun 📖	CompOp	27 math math: tendsto_tsum_div_pow_atTop_integral, LinearMap.BilinForm.toMatrix_basisFun, BoxIntegral.unitPartition.mem_smul_span_iff, Module.Basis.parallelepiped_basisFun, LDL.lowerInv_eq_gramSchmidtBasis, BoxIntegral.unitPartition.integralSum_eq_tsum_div, tendsto_card_div_pow_atTop_volume, basis_toMatrix_basisFun_mul, hasEigenvector_toLin'_diagonal, Matrix.toBilin_basisFun, LinearMap.toMatrix₂_basisFun, basisFun_det, Module.Basis.coePiBasisFun.toMatrix_eq_transpose, PiLp.basisFun_eq_pi_basisFun, Matrix.toLinearMap₂_basisFun, basisFun_apply, ZSpan.fundamentalDomain_pi_basisFun, BilinForm.toMatrix_basisFun, Matrix.toLin_eq_toLin', ZSpan.discreteTopology_pi_basisFun, tendsto_card_div_pow_atTop_volume', LinearMap.toMatrix_eq_toMatrix', basisFun_equivFun, PiLp.basisFun_map, basisFun_repr, basisFun_det_apply, BoxIntegral.unitPartition.tag_mem_smul_span

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
basisFun_apply 📖	mathematical	—	DFunLike.coe Module.Basis addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Function.module Semiring.toModule Module.Basis.instFunLike basisFun single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	RingHomInvPair.ids Module.Basis.coe_ofEquivFun
basisFun_equivFun 📖	mathematical	—	Module.Basis.equivFun addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Function.module Semiring.toModule basisFun LinearEquiv.refl	—	Module.Basis.equivFun_ofEquivFun
basisFun_repr 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.instAddCommMonoid Function.module Semiring.toModule Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr basisFun	—	—
basis_apply 📖	mathematical	—	DFunLike.coe Module.Basis addCommMonoid module Module.Basis.instFunLike basis single AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	RingHomInvPair.ids Module.Basis.apply_eq_iff basis_repr_single Sigma.eta
basis_repr 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids addCommMonoid Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid module Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr basis	—	RingHomInvPair.ids
basis_repr_single 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring addCommMonoid Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid module Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr basis single AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Module.Basis Module.Basis.instFunLike Finsupp.single AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Finsupp.ext RingHomInvPair.ids Module.Basis.repr_symm_apply LinearEquiv.trans.congr_simp Finsupp.single_apply single_eq_same Module.Basis.repr_self single_eq_of_ne map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass Finsupp.zero_apply Finsupp.single_eq_of_ne
linearIndependent_single 📖	mathematical	LinearIndependent	single AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid module	—	LinearIndependent.map_injOn DFinsupp.linearIndependent_single Function.Injective.injOn DFinsupp.injective_pi_lapply
linearIndependent_single_of_ne_zero 📖	mathematical	—	LinearIndependent single NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toSemiring addCommMonoid AddCommGroup.toAddCommMonoid Function.module	—	linearIndependent_equiv linearIndependent_single
linearIndependent_single_one 📖	mathematical	—	LinearIndependent single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Function.module Semiring.toModule	—	linearIndependent_equiv linearIndependent_single Finset.sum_congr Finset.univ_unique mul_one Finset.sum_singleton

---

← Back to Index