Decomposition

📁 Source: Mathlib/LinearAlgebra/TensorProduct/Decomposition.lean

Statistics

Metric	Count
Definitions baseChange	1
Theorems baseChange, toBaseChange_bijective, toBaseChange_injective, toBaseChange_bijective, toBaseChange_injective	5
Total	6

DirectSum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toBaseChange_bijective 📖	mathematical	—	Function.Bijective TensorProduct Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Submodule.addCommMonoid Algebra.toModule Submodule.module TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass Submodule.baseChange DFunLike.coe LinearMap RingHom.id LinearMap.instFunLike Submodule.toBaseChange	—	Submodule.addSubmonoidClass Algebra.to_smulCommClass toBaseChange_injective Submodule.toBaseChange_surjective
toBaseChange_injective 📖	mathematical	—	TensorProduct Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Submodule.addCommMonoid Algebra.toModule Submodule.module TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass Submodule.baseChange DFunLike.coe LinearMap RingHom.id LinearMap.instFunLike Submodule.toBaseChange	—	Submodule.addSubmonoidClass Algebra.to_smulCommClass Function.Bijective.of_comp_iff RingHomInvPair.ids RingHomCompTriple.ids LinearEquiv.coe_trans LinearEquiv.bijective Equiv.bijective of_injective Function.Bijective.injective lmap_of

DirectSum.Decomposition

Definitions

Name	Category	Theorems
baseChange 📖	CompOp	—

DirectSum.IsInternal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
baseChange 📖	mathematical	DirectSum.IsInternal Submodule CommSemiring.toSemiring Submodule.setLike Submodule.addSubmonoidClass	DirectSum.IsInternal TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule Submodule TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass Submodule.setLike Submodule.addSubmonoidClass Submodule.baseChange	—	Submodule.addSubmonoidClass DirectSum.Decomposition.isInternal Algebra.to_smulCommClass
toBaseChange_bijective 📖	mathematical	DirectSum.IsInternal Submodule CommSemiring.toSemiring Submodule.setLike Submodule.addSubmonoidClass	Function.Bijective TensorProduct Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Submodule.addCommMonoid Algebra.toModule Submodule.module TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass Submodule.baseChange DFunLike.coe LinearMap RingHom.id LinearMap.instFunLike Submodule.toBaseChange	—	Submodule.addSubmonoidClass DirectSum.toBaseChange_bijective
toBaseChange_injective 📖	mathematical	DirectSum.IsInternal Submodule CommSemiring.toSemiring Submodule.setLike Submodule.addSubmonoidClass	TensorProduct Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Submodule.addCommMonoid Algebra.toModule Submodule.module TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass Submodule.baseChange DFunLike.coe LinearMap RingHom.id LinearMap.instFunLike Submodule.toBaseChange	—	Submodule.addSubmonoidClass Function.Bijective.injective Algebra.to_smulCommClass toBaseChange_bijective

---

← Back to Index