Documentation Verification Report

BaseChange

📁 Source: Mathlib/RingTheory/Extension/Cotangent/BaseChange.lean

Statistics

Metric	Count
Definitions `tensorCotangentSpace`	1
Theorems `tensorCotangentSpace_tmul`, `tensorCotangentSpace_tmul_tmul`	2
Total	3

Algebra.Extension

Definitions

Name	Category	Theorems
`tensorCotangentSpace` 📖	CompOp	2 math math: `tensorCotangentSpace_tmul_tmul`, `tensorCotangentSpace_tmul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tensorCotangentSpace_tmul` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `CotangentSpace` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `TensorProduct.addCommMonoid` `Ring` `commRing` `KaehlerDifferential` `instRingOfIsScalarTower` `Algebra.id` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Algebra.toModule` `algebra₂` `KaehlerDifferential.module'` `TensorProduct.leftModule` `IsScalarTower.to_smulCommClass'` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `instIsScalarTowerRing_2` `Algebra.TensorProduct.instCommRing` `Algebra.TensorProduct.leftAlgebra` `Algebra.to_smulCommClass` `baseChange` `Semiring.toModule` `TensorProduct.isScalarTower_left` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toSMul` `IsScalarTower.right` `Algebra.TensorProduct.instSemiring` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `tensorCotangentSpace` `TensorProduct.tmul` `TensorProduct.leftHasSMul` `TensorProduct.leftDistribMulAction` `LinearMap` `Algebra.TensorProduct.rightAlgebra` `SMulCommClass.of_commMonoid` `CommRing.toCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `LinearMap.instFunLike` `CotangentSpace.map` `Algebra.TensorProduct.instAlgebra` `toBaseChange`	—	`TensorProduct.induction_on` `Algebra.to_smulCommClass` `RingHomInvPair.ids` `IsScalarTower.to_smulCommClass'` `IsScalarTower.left` `instIsScalarTowerRing_2` `TensorProduct.isScalarTower_left` `IsScalarTower.right` `SMulCommClass.of_commMonoid` `TensorProduct.tmul_zero` `LinearEquiv.map_zero` `LinearMap.map_zero` `smul_zero` `instSMulCommClass` `instIsScalarTowerRingTensorProductBaseChange` `instIsScalarTowerRing_1` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `IsScalarTower.of_algHom` `tensorCotangentSpace_tmul_tmul` `CotangentSpace.map_tmul_eq_tmul_map` `Algebra.smul_def` `mul_one` `one_mul` `TensorProduct.tmul_add` `LinearEquiv.map_add` `LinearMap.map_add` `smul_add`
`tensorCotangentSpace_tmul_tmul` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `CotangentSpace` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `TensorProduct.addCommMonoid` `Ring` `commRing` `KaehlerDifferential` `instRingOfIsScalarTower` `Algebra.id` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Algebra.toModule` `algebra₂` `KaehlerDifferential.module'` `TensorProduct.leftModule` `IsScalarTower.to_smulCommClass'` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `instIsScalarTowerRing_2` `Algebra.TensorProduct.instCommRing` `Algebra.TensorProduct.leftAlgebra` `Algebra.to_smulCommClass` `baseChange` `Semiring.toModule` `TensorProduct.isScalarTower_left` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toSMul` `IsScalarTower.right` `Algebra.TensorProduct.instSemiring` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `tensorCotangentSpace` `TensorProduct.tmul` `LinearMap` `algebraBaseChange` `instSMulCommClass` `LinearMap.instFunLike` `KaehlerDifferential.map` `Algebra.TensorProduct.instAlgebra` `instIsScalarTowerRingTensorProductBaseChange` `instIsScalarTowerRing_1`	—	`IsScalarTower.left` `Algebra.to_smulCommClass` `RingHomInvPair.ids` `IsScalarTower.to_smulCommClass'` `instIsScalarTowerRing_2` `TensorProduct.isScalarTower_left` `IsScalarTower.right` `instSMulCommClass` `instIsScalarTowerRingTensorProductBaseChange` `instIsScalarTowerRing_1` `smulCommClass_self` `TensorProduct.smulCommClass_left` `TensorProduct.mk_apply` `IsTensorProduct.assocOfMapSMul_symm_tmul` `KaehlerDifferential.span_range_derivation` `Submodule.span_induction` `KaehlerDifferential.tensorKaehlerEquiv_tmul_D` `one_smul` `KaehlerDifferential.map_D` `TensorProduct.tmul_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `LinearMap.semilinearMapClass` `TensorProduct.tmul_add` `map_add` `SemilinearMapClass.toAddHomClass` `TensorProduct.tmul_smul` `TensorProduct.CompatibleSMul.isScalarTower` `KaehlerDifferential.isScalarTower_of_tower` `algebraMap_smul` `LinearEquiv.map_smul` `LinearMap.map_smul`

---

← Back to Index