Free

📁 Source: Mathlib/RingTheory/TensorProduct/Free.lean

Statistics

Metric	Count
Definitions basis, basisAux	2
Theorems basisAux_map_smul, basisAux_tmul, basis_apply, basis_repr_symm_apply, basis_repr_symm_apply', basis_repr_tmul, instFree, toMatrix_baseChange, baseChange_end, baseChange_linearMap	10
Total	12

Algebra.TensorProduct

Definitions

Name	Category	Theorems
basis 📖	CompOp	11 math math: basis_apply, LinearMap.toMatrix_baseChange, basis_repr_tmul, LinearMap.polyCharpoly_baseChange, LinearMap.toMvPolynomial_baseChange, Module.Basis.baseChange_end, basis_repr_symm_apply', LinearMap.polyCharpolyAux_baseChange, LinearMap.polyCharpolyAux_map_aeval, basis_repr_symm_apply, Module.Basis.baseChange_linearMap
basisAux 📖	CompOp	2 math math: basisAux_map_smul, basisAux_tmul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
basisAux_map_smul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass TensorProduct.addCommMonoid Finsupp.instAddCommMonoid TensorProduct.instModule Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv basisAux TensorProduct.leftHasSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Semiring.toModule Algebra.to_smulCommClass SMulZeroClass.toSMul Finsupp.instZero Finsupp.smulZeroClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instDistribSMul	—	TensorProduct.induction_on RingHomInvPair.ids Algebra.to_smulCommClass smul_zero map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass basisAux_tmul smul_assoc Finsupp.isScalarTower IsScalarTower.left smul_add map_add SemilinearMapClass.toAddHomClass
basisAux_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass TensorProduct.addCommMonoid Finsupp.instAddCommMonoid TensorProduct.instModule Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv basisAux TensorProduct.tmul SMulZeroClass.toSMul Finsupp.instZero Finsupp.smulZeroClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instDistribSMul Finsupp.mapRange RingHom RingHom.instFunLike algebraMap map_zero MonoidWithZeroHomClass.toZeroHomClass NonAssocSemiring.toMulZeroOneClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Semiring.toModule Module.Basis.repr	—	Finsupp.ext RingHomInvPair.ids map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Finsupp.LinearEquiv.finsuppUnique_symm_apply Finsupp.smulCommClass IsScalarTower.to_smulCommClass finsuppTensorFinsupp_apply Finsupp.single_eq_same Algebra.smul_def
basis_apply 📖	mathematical	—	DFunLike.coe Module.Basis TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass Module.Basis.instFunLike basis TensorProduct.tmul AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne CommSemiring.toSemiring	—	basis_repr_symm_apply
basis_repr_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toModule Finsupp.instAddCommMonoid TensorProduct.addCommMonoid Finsupp.module Semiring.toModule TensorProduct.leftModule Algebra.to_smulCommClass EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm Module.Basis.repr basis Finsupp.single TensorProduct.tmul CommSemiring.toSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	RingHomInvPair.ids Algebra.to_smulCommClass basisAux_map_smul LinearEquiv.trans.congr_simp Finsupp.lcongr_symm Finsupp.lcongr_single finsuppTensorFinsupp_symm_single Finsupp.single_eq_same Module.Basis.repr_symm_apply Finsupp.linearCombination_single one_smul
basis_repr_symm_apply' 📖	mathematical	—	TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule TensorProduct.leftHasSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Semiring.toModule Algebra.to_smulCommClass DFunLike.coe Module.Basis TensorProduct.addCommMonoid TensorProduct.leftModule Module.Basis.instFunLike basis TensorProduct.tmul CommSemiring.toSemiring	—	Algebra.to_smulCommClass basis_apply RingHomInvPair.ids Module.Basis.repr_symm_apply Finsupp.linearCombination_single one_smul basis_repr_symm_apply
basis_repr_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass TensorProduct.addCommMonoid Finsupp.instAddCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr basis TensorProduct.tmul SMulZeroClass.toSMul Finsupp.instZero Finsupp.smulZeroClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instDistribSMul Finsupp.mapRange CommSemiring.toSemiring RingHom RingHom.instFunLike algebraMap map_zero MonoidWithZeroHomClass.toZeroHomClass NonAssocSemiring.toMulZeroOneClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass	—	basisAux_tmul
instFree 📖	mathematical	—	Module.Free TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass	—	Module.Free.of_basis Algebra.to_smulCommClass

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toMatrix_baseChange 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass Matrix addCommMonoid Matrix.addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix Algebra.TensorProduct.basis baseChange Matrix.map RingHom RingHom.instFunLike algebraMap	—	Matrix.ext RingHomInvPair.ids Algebra.to_smulCommClass smulCommClass_self map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass toMatrix_apply Algebra.TensorProduct.basis_apply Algebra.TensorProduct.basis_repr_tmul one_smul

Module.Basis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
baseChange_end 📖	mathematical	—	LinearMap.baseChange CommSemiring.toSemiring DFunLike.coe Module.Basis Module.End LinearMap.addCommMonoid RingHom.id Semiring.toNonAssocSemiring LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instFunLike end TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass Algebra.TensorProduct.basis	—	baseChange_linearMap
baseChange_linearMap 📖	mathematical	—	LinearMap.baseChange CommSemiring.toSemiring DFunLike.coe Module.Basis LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instFunLike linearMap TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass Algebra.TensorProduct.basis	—	ext Algebra.to_smulCommClass smulCommClass_self Algebra.TensorProduct.basis_apply linearMap_apply_apply TensorProduct.tmul_zero

---

← Back to Index