Documentation Verification Report

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`	`IsBaseChange` `DirectSum` `instAddCommMonoidDirectSum` `DirectSum.instModule` `CommSemiring.toSemiring` `DirectSum.instIsScalarTower` `Algebra.toSMul` `DirectSum.lmap`	—	`of_equiv` `DirectSum.instIsScalarTower` `Algebra.to_smulCommClass` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `RingHomCompTriple.ids` `RingHomInvPair.ids` `DirectSum.ext` `IsScalarTower.left` `TensorProduct.coe_directSumRight` `TensorProduct.directSumRight_tmul` `one_smul`
`directSumPow` 📖	mathematical	`IsBaseChange`	`IsBaseChange` `DirectSum` `instAddCommMonoidDirectSum` `DirectSum.instModule` `CommSemiring.toSemiring` `DirectSum.instIsScalarTower` `Algebra.toSMul` `DirectSum.lmap`	—	`directSum`
`finitePow` 📖	mathematical	`IsBaseChange`	`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`	`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`	`IsBaseChange` `Pi.addCommMonoid` `Pi.module` `CommSemiring.toSemiring` `Pi.isScalarTower` `Algebra.toSMul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `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`	`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`	`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