Bilinear

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

Statistics

Metric	Count
Definitions	0
Theorems ext_basis, sum_repr_mul_repr_mul, sum_repr_mul_repr_mulₛₗ	3
Total	3

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext_basis 📖	—	DFunLike.coe LinearMap instFunLike addCommMonoid module Module.Basis Module.Basis.instFunLike	—	—	Module.Basis.ext
sum_repr_mul_repr_mul 📖	mathematical	—	Finsupp.sum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids Finsupp Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule EquivLike.toFunLike LinearEquiv.instEquivLike Module.Basis.repr SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction LinearMap instFunLike addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Module.Basis Module.Basis.instFunLike	—	smulCommClass_self RingHomInvPair.ids Module.Basis.linearCombination_repr Finset.sum_congr map_sum₂ map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass semilinearMapClass map_smul₂ map_smul SemilinearMapClass.toMulActionSemiHomClass
sum_repr_mul_repr_mulₛₗ 📖	mathematical	—	Finsupp.sum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids Finsupp Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule EquivLike.toFunLike LinearEquiv.instEquivLike Module.Basis.repr SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction RingHom RingHom.instFunLike LinearMap instFunLike addCommMonoid module Module.Basis Module.Basis.instFunLike	—	RingHomInvPair.ids Module.Basis.linearCombination_repr Finset.sum_congr map_sum₂ map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass semilinearMapClass map_smulₛₗ₂ MulActionSemiHomClass.map_smulₛₗ SemilinearMapClass.toMulActionSemiHomClass

---

← Back to Index