IsBaseChangePi

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

Statistics

Metric	Count
Definitions	0
Theorems directSum, directSumPow, finitePow, finsuppPow, pi, prodMap, pi, prodMap	8
Total	8

IsBaseChange

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
directSum 📖	mathematical	IsScalarTower Algebra.toSMul CommSemiring.toSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBaseChange	DirectSum instAddCommMonoidDirectSum DirectSum.instModule DirectSum.instIsScalarTower DirectSum.lmap	—	of_equiv DirectSum.instIsScalarTower Algebra.to_smulCommClass IsScalarTower.to_smulCommClass IsScalarTower.right RingHomCompTriple.ids RingHomInvPair.ids DirectSum.ext TensorProduct.directSumRight_tmul one_smul
directSumPow 📖	mathematical	IsBaseChange	DirectSum instAddCommMonoidDirectSum DirectSum.instModule CommSemiring.toSemiring DirectSum.instIsScalarTower Algebra.toSMul DirectSum.lmap	—	directSum
finitePow 📖	mathematical	IsBaseChange	Pi.addCommMonoid Pi.Function.module CommSemiring.toSemiring Pi.isScalarTower Algebra.toSMul SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction LinearMap.compLeft	—	pi
finsuppPow 📖	mathematical	IsBaseChange	Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module CommSemiring.toSemiring Finsupp.isScalarTower DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.toSMul Finsupp.mapRange.linearMap RingHom.id Semiring.toNonAssocSemiring	—	of_equiv Finsupp.isScalarTower Algebra.to_smulCommClass RingHomCompTriple.ids RingHomInvPair.ids DirectSum.instIsScalarTower directSum LinearEquiv.trans_apply LinearMap.map_zero Finsupp.mapRange.linearMap_apply LinearEquiv.symm_apply_eq DirectSum.ext lmap_finsuppLEquivDirectSum_eq one_smul finsuppLEquivDirectSum_apply
pi 📖	mathematical	IsScalarTower Algebra.toSMul CommSemiring.toSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBaseChange	Pi.addCommMonoid Pi.module Pi.isScalarTower SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction LinearMap.pi LinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearMap.proj	—	nonempty_fintype Pi.isScalarTower RingHomCompTriple.ids of_equiv Algebra.to_smulCommClass IsScalarTower.to_smulCommClass IsScalarTower.right RingHomInvPair.ids TensorProduct.piRight_apply one_smul
prodMap 📖	mathematical	IsBaseChange	Prod.instAddCommMonoid Prod.instModule CommSemiring.toSemiring Prod.isScalarTower SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul LinearMap.prodMap	—	of_equiv Prod.isScalarTower Algebra.to_smulCommClass IsScalarTower.to_smulCommClass IsScalarTower.right RingHomCompTriple.ids RingHomInvPair.ids one_smul

IsLocalizedModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pi 📖	mathematical	IsLocalizedModule	Pi.addCommMonoid Pi.module CommSemiring.toSemiring LinearMap.pi LinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearMap.proj	—	RingHomCompTriple.ids Localization.isLocalization Pi.isScalarTower isScalarTower_module isLocalizedModule_iff_isBaseChange IsBaseChange.pi
prodMap 📖	mathematical	—	IsLocalizedModule Prod.instAddCommMonoid Prod.instModule CommSemiring.toSemiring LinearMap.prodMap	—	Localization.isLocalization Prod.isScalarTower isScalarTower_module isLocalizedModule_iff_isBaseChange IsBaseChange.prodMap

---

← Back to Index