Basis

📁 Source: Mathlib/LinearAlgebra/Dual/Basis.lean

Statistics

Metric	Count
Definitions dualBasis, toDual, toDualEquiv, toDualFlip, DualBases, basis, coeffs, lc, evalUseFiniteInstance, tacticUse_finite_instance	10
Theorems coe_dualBasis, coe_toDual_self, coord_toDualEquiv_symm_apply, dualBasis_apply, dualBasis_apply_self, dualBasis_coord_toDualEquiv_apply, dualBasis_equivFun, dualBasis_repr, eval_injective, eval_ker, eval_range, linearCombination_coord, linearCombination_dualBasis, sum_dual_apply_smul_coord, toDualEquiv_apply, toDualFlip_apply, toDual_apply, toDual_apply_left, toDual_apply_right, toDual_eq_equivFun, toDual_eq_repr, toDual_inj, toDual_injective, toDual_ker, toDual_linearCombination_left, toDual_linearCombination_right, toDual_range, toDual_toDual, basis_repr_apply, basis_repr_symm_apply, coe_basis, coe_dualBasis, coeffs_apply, coeffs_lc, dual_lc, eval_of_ne, eval_same, finite, lc_coeffs, lc_def, mem_of_mem_span, total	42
Total	52

Module

Definitions

Name	Category	Theorems
DualBases 📖	CompData	—

Module.Basis

Definitions

Name	Category	Theorems
dualBasis 📖	CompOp	15 math math: dualBasis_coord_toDualEquiv_apply, flag_le_ker_dual, coe_dualBasis, Module.DualBases.coe_dualBasis, LinearMap.toMatrix_transpose, dualBasis_apply_self, dualBasis_equivFun, linearCombination_dualBasis, PiTensorProduct.dualDistribInvOfBasis_apply, toDual_toDual, dualBasis_apply, dualBasis_repr, TensorProduct.dualDistribInvOfBasis_apply, Matrix.toLin_transpose, coord_toDualEquiv_symm_apply
toDual 📖	CompOp	14 math math: toDual_linearCombination_left, toDualEquiv_apply, toDual_ker, toDual_range, toDual_eq_repr, toDual_toDual, toDual_injective, toDual_apply, coe_toDual_self, toDual_linearCombination_right, toDualFlip_apply, toDual_apply_left, toDual_apply_right, toDual_eq_equivFun
toDualEquiv 📖	CompOp	3 math math: dualBasis_coord_toDualEquiv_apply, toDualEquiv_apply, coord_toDualEquiv_symm_apply
toDualFlip 📖	CompOp	1 math math: toDualFlip_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_dualBasis 📖	mathematical	—	DFunLike.coe Module.Basis Module.Dual CommSemiring.toSemiring LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instFunLike dualBasis coord	—	smulCommClass_self LinearMap.ext dualBasis_apply
coe_toDual_self 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Module.Dual LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike toDual Module.Basis instFunLike coord	—	LinearMap.ext smulCommClass_self toDual_apply_right
coord_toDualEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike coord LinearEquiv RingHomInvPair.ids Module.Dual LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm toDualEquiv dualBasis	—	RingHomInvPair.ids smulCommClass_self
dualBasis_apply 📖	mathematical	—	DFunLike.coe Module.Dual CommSemiring.toSemiring LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id Module.Basis LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instFunLike dualBasis Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Finsupp.instFunLike LinearEquiv RingHomInvPair.ids Finsupp.instAddCommMonoid Finsupp.module EquivLike.toFunLike LinearEquiv.instEquivLike repr	—	toDual_apply_right
dualBasis_apply_self 📖	mathematical	—	DFunLike.coe Module.Dual CommSemiring.toSemiring LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id Module.Basis LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instFunLike dualBasis AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	smulCommClass_self toDual_apply
dualBasis_coord_toDualEquiv_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Module.Dual LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike coord dualBasis LinearEquiv RingHomInvPair.ids EquivLike.toFunLike LinearEquiv.instEquivLike toDualEquiv	—	smulCommClass_self RingHomInvPair.ids LinearEquiv.symm_apply_apply
dualBasis_equivFun 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Module.Dual LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Pi.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Pi.Function.module EquivLike.toFunLike LinearEquiv.instEquivLike equivFun dualBasis LinearMap.instFunLike Module.Basis instFunLike	—	RingHomInvPair.ids smulCommClass_self equivFun_apply dualBasis_repr
dualBasis_repr 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids Module.Dual LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule Finsupp.instAddCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Finsupp.module EquivLike.toFunLike LinearEquiv.instEquivLike repr dualBasis LinearMap.instFunLike Module.Basis instFunLike	—	RingHomInvPair.ids smulCommClass_self linearCombination_dualBasis linearCombination_repr
eval_injective 📖	mathematical	—	Module.Dual CommSemiring.toSemiring LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction DFunLike.coe LinearMap LinearMap.instFunLike Module.Dual.eval	—	smulCommClass_self ext_elem
eval_ker 📖	mathematical	—	LinearMap.ker Module.Dual CommSemiring.toSemiring LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Module.Dual.eval Bot.bot Submodule Submodule.instBot	—	LinearMap.ker_eq_bot_of_injective smulCommClass_self eval_injective
eval_range 📖	mathematical	—	LinearMap.range Module.Dual CommSemiring.toSemiring LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction RingHomSurjective.ids Module.Dual.eval Top.top Submodule Submodule.instTop	—	nonempty_fintype smulCommClass_self RingHomSurjective.ids RingHomCompTriple.ids toDual_toDual LinearMap.range_comp toDual_range Submodule.map_top
linearCombination_coord 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Finsupp.instAddCommMonoid LinearMap.addCommMonoid Finsupp.module LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Finsupp.linearCombination coord Module.Basis instFunLike Finsupp.instFunLike	—	smulCommClass_self coe_dualBasis linearCombination_dualBasis
linearCombination_dualBasis 📖	mathematical	—	DFunLike.coe Module.Dual CommSemiring.toSemiring LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Finsupp.instAddCommMonoid LinearMap.addCommMonoid Finsupp.module LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Finsupp.linearCombination Module.Basis instFunLike dualBasis Finsupp.instFunLike	—	nonempty_fintype smulCommClass_self Finsupp.linearCombination_apply Finsupp.sum_fintype zero_smul LinearMap.sum_apply Finset.sum_congr dualBasis_apply_self mul_boole Finset.sum_ite_eq Finset.mem_univ
sum_dual_apply_smul_coord 📖	mathematical	—	Finset.sum LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid Finset.univ LinearMap.instSMul instDistribSMul smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction DFunLike.coe Module.Dual LinearMap.instFunLike Module.Basis instFunLike coord	—	LinearMap.ext smulCommClass_self LinearMap.sum_apply Finset.sum_congr mul_comm LinearMap.map_smul DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass RingHomInvPair.ids sum_repr
toDualEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Module.Dual LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike LinearEquiv.instEquivLike toDualEquiv LinearMap LinearMap.instFunLike toDual	—	RingHomInvPair.ids smulCommClass_self
toDualFlip_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike toDualFlip Module.Dual LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction toDual	—	—
toDual_apply 📖	mathematical	—	DFunLike.coe Module.Dual CommSemiring.toSemiring LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction toDual Module.Basis instFunLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	smulCommClass_self RingHomInvPair.ids toDual.eq_1 constr_basis
toDual_apply_left 📖	mathematical	—	DFunLike.coe Module.Dual CommSemiring.toSemiring LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction toDual Module.Basis instFunLike Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Finsupp.instFunLike LinearEquiv RingHomInvPair.ids Finsupp.instAddCommMonoid Finsupp.module EquivLike.toFunLike LinearEquiv.instEquivLike repr	—	smulCommClass_self RingHomInvPair.ids toDual_linearCombination_left linearCombination_repr
toDual_apply_right 📖	mathematical	—	DFunLike.coe Module.Dual CommSemiring.toSemiring LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction toDual Module.Basis instFunLike Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Finsupp.instFunLike LinearEquiv RingHomInvPair.ids Finsupp.instAddCommMonoid Finsupp.module EquivLike.toFunLike LinearEquiv.instEquivLike repr	—	smulCommClass_self RingHomInvPair.ids toDual_linearCombination_right linearCombination_repr
toDual_eq_equivFun 📖	mathematical	—	DFunLike.coe Module.Dual CommSemiring.toSemiring LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction toDual Module.Basis instFunLike LinearEquiv RingHomInvPair.ids Pi.addCommMonoid Pi.Function.module EquivLike.toFunLike LinearEquiv.instEquivLike equivFun	—	smulCommClass_self RingHomInvPair.ids equivFun_apply toDual_eq_repr
toDual_eq_repr 📖	mathematical	—	DFunLike.coe Module.Dual CommSemiring.toSemiring LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction toDual Module.Basis instFunLike Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Finsupp.instFunLike LinearEquiv RingHomInvPair.ids Finsupp.instAddCommMonoid Finsupp.module EquivLike.toFunLike LinearEquiv.instEquivLike repr	—	toDual_apply_left
toDual_inj 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Module.Dual LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike toDual LinearMap.instZero	AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	smulCommClass_self toDual_injective map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
toDual_injective 📖	mathematical	—	Module.Dual CommSemiring.toSemiring DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike toDual	—	smulCommClass_self RingHomInvPair.ids ext_elem_iff DFunLike.congr_fun
toDual_ker 📖	mathematical	—	LinearMap.ker Module.Dual CommSemiring.toSemiring LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction toDual Bot.bot Submodule Submodule.instBot	—	smulCommClass_self LinearMap.ker_eq_bot'
toDual_linearCombination_left 📖	mathematical	—	DFunLike.coe Module.Dual CommSemiring.toSemiring LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction toDual Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Finsupp.instAddCommMonoid Finsupp.module Finsupp.linearCombination Module.Basis instFunLike Finsupp.instFunLike	—	smulCommClass_self Finsupp.linearCombination_apply Finsupp.sum.eq_1 map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass LinearMap.sum_apply Finset.sum_congr map_smul SemilinearMapClass.toMulActionSemiHomClass toDual_apply mul_boole Finset.sum_ite_eq' Finsupp.if_mem_support
toDual_linearCombination_right 📖	mathematical	—	DFunLike.coe Module.Dual CommSemiring.toSemiring LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction toDual Module.Basis instFunLike Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Finsupp.instAddCommMonoid Finsupp.module Finsupp.linearCombination Finsupp.instFunLike	—	smulCommClass_self Finsupp.linearCombination_apply Finsupp.sum.eq_1 map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finset.sum_congr map_smul SemilinearMapClass.toMulActionSemiHomClass toDual_apply mul_boole Finset.sum_ite_eq Finsupp.if_mem_support
toDual_range 📖	mathematical	—	LinearMap.range Module.Dual CommSemiring.toSemiring LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction RingHomSurjective.ids toDual Top.top Submodule Submodule.instTop	—	smulCommClass_self RingHomSurjective.ids Submodule.eq_top_iff' ext toDual_linearCombination_left
toDual_toDual 📖	mathematical	—	LinearMap.comp Module.Dual CommSemiring.toSemiring LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction RingHomCompTriple.ids toDual dualBasis Module.Dual.eval	—	ext smulCommClass_self RingHomCompTriple.ids LinearMap.comp_apply RingHomInvPair.ids toDual_apply_left coe_toDual_self coe_dualBasis Module.Dual.eval_apply repr_self Finsupp.single_apply dualBasis_apply_self

Module.DualBases

Definitions

Name	Category	Theorems
basis 📖	CompOp	4 math math: basis_repr_symm_apply, coe_dualBasis, basis_repr_apply, coe_basis
coeffs 📖	CompOp	4 math math: lc_coeffs, basis_repr_apply, coeffs_lc, coeffs_apply
lc 📖	CompOp	5 math math: basis_repr_symm_apply, lc_coeffs, dual_lc, coeffs_lc, lc_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
basis_repr_apply 📖	mathematical	Module.DualBases	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule EquivLike.toFunLike LinearEquiv.instEquivLike Module.Basis.repr basis coeffs	—	—
basis_repr_symm_apply 📖	mathematical	Module.DualBases	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm Module.Basis.repr basis lc	—	—
coe_basis 📖	mathematical	Module.DualBases	DFunLike.coe Module.Basis CommSemiring.toSemiring Module.Basis.instFunLike basis	—	RingHomInvPair.ids Module.Basis.apply_eq_iff Finsupp.ext eq_or_ne eval_same Finsupp.single_eq_same eval_of_ne Finsupp.single_eq_of_ne'
coe_dualBasis 📖	mathematical	Module.DualBases	DFunLike.coe Module.Basis Module.Dual CommSemiring.toSemiring LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Module.Basis.instFunLike Module.Basis.dualBasis basis	—	smulCommClass_self Module.Basis.ext Module.Basis.coe_dualBasis coe_basis
coeffs_apply 📖	mathematical	Module.DualBases	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Finsupp.instFunLike coeffs Module.Dual LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule RingHom.id	—	—
coeffs_lc 📖	mathematical	Module.DualBases	coeffs lc	—	Finsupp.ext coeffs_apply dual_lc
dual_lc 📖	mathematical	Module.DualBases	DFunLike.coe Module.Dual CommSemiring.toSemiring LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id lc Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Finsupp.instFunLike	—	lc.eq_1 map_finsuppSum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finsupp.sum_eq_single map_smul SemilinearMapClass.toMulActionSemiHomClass eval_of_ne MulZeroClass.mul_zero zero_smul map_zero AddMonoidHomClass.toZeroHomClass eval_same mul_one
eval_of_ne 📖	mathematical	Module.DualBases	Pairwise DFunLike.coe Module.Dual CommSemiring.toSemiring LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—
eval_same 📖	mathematical	Module.DualBases	DFunLike.coe Module.Dual CommSemiring.toSemiring LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—
finite 📖	mathematical	Module.DualBases	Set.Finite setOf DFunLike.coe Module.Dual CommSemiring.toSemiring LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—
lc_coeffs 📖	mathematical	Module.DualBases	lc coeffs	—	total dual_lc
lc_def 📖	mathematical	—	lc DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule LinearMap.instFunLike Finsupp.linearCombination	—	—
mem_of_mem_span 📖	mathematical	Module.DualBases Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike Submodule.span Set.image	Set Set.instMembership	—	Finsupp.mem_span_image_iff_linearCombination not_imp_comm Finsupp.mem_supported' dual_lc lc_def
total 📖	—	Module.DualBases DFunLike.coe Module.Dual CommSemiring.toSemiring LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id	—	—	—

(root)

Definitions

Name	Category	Theorems
evalUseFiniteInstance 📖	CompOp	—
tacticUse_finite_instance 📖	CompOp	—

---

← Back to Index