TensorProduct

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

Statistics

Metric	Count
Definitions derivationTensorProduct, moduleBaseChange, moduleBaseChange', mulActionBaseChange, tensorKaehlerEquiv, tensorKaehlerEquivBase	6
Theorems derivationTensorProduct_algebraMap, instIsScalarTowerTensorProduct, instIsScalarTowerTensorProduct_1, instIsScalarTowerTensorProduct_2, instSMulCommClassTensorProduct, instSMulCommClassTensorProduct_1, isBaseChange, isLocalizedModule, isLocalizedModule_of_isLocalizedModule, map_liftBaseChange_smul, mulActionBaseChange_smul_add, mulActionBaseChange_smul_tmul, mulActionBaseChange_smul_zero, tensorKaehlerEquivBase_symm_apply, tensorKaehlerEquivBase_tmul, tensorKaehlerEquiv_left_inv, tensorKaehlerEquiv_symm_D_tmul, tensorKaehlerEquiv_symm_D_tmul', tensorKaehlerEquiv_tmul, tensorKaehlerEquiv_tmul_D	20
Total	26

KaehlerDifferential

Definitions

Name	Category	Theorems
derivationTensorProduct 📖	CompOp	3 math math: tensorKaehlerEquivBase_symm_apply, tensorKaehlerEquiv_left_inv, derivationTensorProduct_algebraMap
moduleBaseChange 📖	CompOp	4 math math: instIsScalarTowerTensorProduct, instSMulCommClassTensorProduct_1, instSMulCommClassTensorProduct, instIsScalarTowerTensorProduct_1
moduleBaseChange' 📖	CompOp	6 math math: tensorKaehlerEquivBase_symm_apply, tensorKaehlerEquiv_left_inv, derivationTensorProduct_algebraMap, instIsScalarTowerTensorProduct_1, map_liftBaseChange_smul, instIsScalarTowerTensorProduct_2
mulActionBaseChange 📖	CompOp	3 math math: mulActionBaseChange_smul_add, mulActionBaseChange_smul_zero, mulActionBaseChange_smul_tmul
tensorKaehlerEquiv 📖	CompOp	3 math math: tensorKaehlerEquiv_symm_D_tmul', tensorKaehlerEquiv_symm_D_tmul, tensorKaehlerEquiv_tmul_D
tensorKaehlerEquivBase 📖	CompOp	3 math math: tensorKaehlerEquivBase_tmul, tensorKaehlerEquivBase_symm_apply, tensorKaehlerEquiv_tmul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
derivationTensorProduct_algebraMap 📖	mathematical	—	DFunLike.coe Derivation TensorProduct CommRing.toCommSemiring KaehlerDifferential NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential Algebra.toModule CommSemiring.toSemiring module' SMulCommClass.of_commMonoid CommRing.toCommMonoid Algebra.toSMul IsScalarTower.right TensorProduct.addCommMonoid moduleBaseChange' TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass Derivation.instFunLike derivationTensorProduct RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap TensorProduct.tmul AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Algebra.id smulCommClass_self DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring D	—	IsBaseChange.lift_eq SMulCommClass.of_commMonoid IsScalarTower.right Algebra.to_smulCommClass TensorProduct.isScalarTower_left
instIsScalarTowerTensorProduct 📖	mathematical	—	IsScalarTower TensorProduct CommRing.toCommSemiring KaehlerDifferential NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential Algebra.toModule CommSemiring.toSemiring module' SMulCommClass.of_commMonoid CommRing.toCommMonoid Algebra.toSMul IsScalarTower.right SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero TensorProduct.addZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero TensorProduct.addMonoid Module.toDistribMulAction TensorProduct.addCommMonoid moduleBaseChange TensorProduct.instSMul	—	IsScalarTower.of_algebraMap_smul SMulCommClass.of_commMonoid IsScalarTower.right TensorProduct.induction_on smul_zero Algebra.to_smulCommClass mulActionBaseChange_smul_tmul algebraMap_smul isScalarTower_of_tower TensorProduct.tmul_smul TensorProduct.CompatibleSMul.isScalarTower IsScalarTower.left smul_add
instIsScalarTowerTensorProduct_1 📖	mathematical	—	IsScalarTower TensorProduct CommRing.toCommSemiring KaehlerDifferential NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential Algebra.toModule CommSemiring.toSemiring module' SMulCommClass.of_commMonoid CommRing.toCommMonoid Algebra.toSMul IsScalarTower.right SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero TensorProduct.addZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero TensorProduct.addMonoid Module.toDistribMulAction TensorProduct.addCommMonoid moduleBaseChange' moduleBaseChange	—	IsScalarTower.of_algebraMap_smul SMulCommClass.of_commMonoid IsScalarTower.right Algebra.to_smulCommClass IsScalarTower.to_smulCommClass' TensorProduct.isScalarTower_left TensorProduct.smulCommClass_left instIsScalarTowerTensorProduct instSMulCommClassTensorProduct_1 LinearMap.ext SMulCommClass.smul_comm instSMulCommClassTensorProduct Algebra.pushoutDesc_right
instIsScalarTowerTensorProduct_2 📖	mathematical	—	IsScalarTower TensorProduct CommRing.toCommSemiring KaehlerDifferential NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential Algebra.toModule CommSemiring.toSemiring module' SMulCommClass.of_commMonoid CommRing.toCommMonoid Algebra.toSMul IsScalarTower.right SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero TensorProduct.addZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero TensorProduct.addMonoid Module.toDistribMulAction TensorProduct.addCommMonoid moduleBaseChange' TensorProduct.leftHasSMul Semiring.toModule Algebra.to_smulCommClass	—	IsScalarTower.of_algebraMap_smul SMulCommClass.of_commMonoid IsScalarTower.right Algebra.to_smulCommClass IsScalarTower.to_smulCommClass' TensorProduct.isScalarTower_left TensorProduct.smulCommClass_left instIsScalarTowerTensorProduct instSMulCommClassTensorProduct_1 LinearMap.ext SMulCommClass.smul_comm instSMulCommClassTensorProduct Algebra.pushoutDesc_left
instSMulCommClassTensorProduct 📖	mathematical	—	SMulCommClass TensorProduct CommRing.toCommSemiring KaehlerDifferential NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential Algebra.toModule CommSemiring.toSemiring module' SMulCommClass.of_commMonoid CommRing.toCommMonoid Algebra.toSMul IsScalarTower.right TensorProduct.leftHasSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Semiring.toModule Algebra.to_smulCommClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero TensorProduct.addZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul TensorProduct.addMonoid TensorProduct.addCommMonoid moduleBaseChange	—	SMulCommClass.of_commMonoid IsScalarTower.right Algebra.to_smulCommClass TensorProduct.induction_on smul_zero mulActionBaseChange_smul_tmul TensorProduct.smul_tmul' smul_add
instSMulCommClassTensorProduct_1 📖	mathematical	—	SMulCommClass TensorProduct CommRing.toCommSemiring KaehlerDifferential NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential Algebra.toModule CommSemiring.toSemiring module' SMulCommClass.of_commMonoid CommRing.toCommMonoid Algebra.toSMul IsScalarTower.right SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero TensorProduct.addZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero TensorProduct.addMonoid Module.toDistribMulAction TensorProduct.addCommMonoid moduleBaseChange TensorProduct.leftHasSMul Semiring.toModule Algebra.to_smulCommClass	—	SMulCommClass.of_commMonoid IsScalarTower.right Algebra.to_smulCommClass SMulCommClass.smul_comm instSMulCommClassTensorProduct
isBaseChange 📖	mathematical	—	IsBaseChange KaehlerDifferential AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential CommRing.toCommSemiring module' SMulCommClass.of_commMonoid CommRing.toCommMonoid Algebra.toSMul CommSemiring.toSemiring IsScalarTower.right isScalarTower_of_tower LinearMap.restrictScalars Algebra.id Algebra.to_smulCommClass LinearMap.IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction map	—	SMulCommClass.of_commMonoid IsScalarTower.right isScalarTower_of_tower Algebra.to_smulCommClass LinearMap.IsScalarTower.compatibleSMul RingHomCompTriple.ids TensorProduct.isScalarTower_left RingHomInvPair.ids TensorProduct.smulCommClass_left smulCommClass_self LinearMap.ext tensorKaehlerEquivBase_tmul one_smul IsBaseChange.comp IsScalarTower.left TensorProduct.isBaseChange IsBaseChange.ofEquiv
isLocalizedModule 📖	mathematical	—	IsLocalizedModule CommRing.toCommSemiring KaehlerDifferential AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential module' SMulCommClass.of_commMonoid CommRing.toCommMonoid Algebra.toSMul CommSemiring.toSemiring IsScalarTower.right LinearMap.restrictScalars Algebra.id Algebra.to_smulCommClass LinearMap.IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction isScalarTower_of_tower map	—	Algebra.IsPushout.symm Algebra.isPushout_of_isLocalization SMulCommClass.of_commMonoid IsScalarTower.right Algebra.to_smulCommClass LinearMap.IsScalarTower.compatibleSMul isScalarTower_of_tower isLocalizedModule_iff_isBaseChange isBaseChange
isLocalizedModule_of_isLocalizedModule 📖	mathematical	—	IsLocalizedModule CommRing.toCommSemiring KaehlerDifferential AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential module' SMulCommClass.of_commMonoid CommRing.toCommMonoid Algebra.toSMul CommSemiring.toSemiring IsScalarTower.right LinearMap.restrictScalars Algebra.id Algebra.to_smulCommClass LinearMap.IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction isScalarTower_of_tower map	—	isLocalizedModule_iff_isLocalization SMulCommClass.of_commMonoid IsScalarTower.right Algebra.to_smulCommClass LinearMap.IsScalarTower.compatibleSMul isScalarTower_of_tower isLocalizedModule
map_liftBaseChange_smul 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct KaehlerDifferential NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential Algebra.toModule module' SMulCommClass.of_commMonoid CommRing.toCommMonoid Algebra.toSMul IsScalarTower.right TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass LinearMap.instFunLike LinearMap.liftBaseChange isScalarTower_of_tower LinearMap.restrictScalars Algebra.id LinearMap.IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction map TensorProduct.addZeroClass TensorProduct.addMonoid moduleBaseChange' SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	SMulCommClass.of_commMonoid IsScalarTower.right IsBaseChange.inductionOn Algebra.IsPushout.out Algebra.to_smulCommClass isScalarTower_of_tower LinearMap.IsScalarTower.compatibleSMul zero_smul map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass TensorProduct.induction_on smul_zero algebraMap_smul instIsScalarTowerTensorProduct_1 map_smul SemilinearMapClass.toMulActionSemiHomClass SMulCommClass.smul_comm IsScalarTower.to_smulCommClass' smul_add map_add SemilinearMapClass.toAddHomClass smul_assoc instIsScalarTowerTensorProduct_2 add_smul
mulActionBaseChange_smul_add 📖	mathematical	—	TensorProduct CommRing.toCommSemiring KaehlerDifferential NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential Algebra.toModule CommSemiring.toSemiring module' SMulCommClass.of_commMonoid CommRing.toCommMonoid Algebra.toSMul IsScalarTower.right SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction mulActionBaseChange TensorProduct.add	—	SMulCommClass.of_commMonoid IsScalarTower.right RingHomInvPair.ids Algebra.to_smulCommClass IsScalarTower.to_smulCommClass isScalarTower_of_tower map_add SemilinearMapClass.toAddHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass smul_add
mulActionBaseChange_smul_tmul 📖	mathematical	—	TensorProduct CommRing.toCommSemiring KaehlerDifferential NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential Algebra.toModule CommSemiring.toSemiring module' SMulCommClass.of_commMonoid CommRing.toCommMonoid Algebra.toSMul IsScalarTower.right SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction mulActionBaseChange TensorProduct.tmul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction Algebra.id Algebra.to_smulCommClass	—	SMulCommClass.of_commMonoid IsScalarTower.right
mulActionBaseChange_smul_zero 📖	mathematical	—	TensorProduct CommRing.toCommSemiring KaehlerDifferential NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential Algebra.toModule CommSemiring.toSemiring module' SMulCommClass.of_commMonoid CommRing.toCommMonoid Algebra.toSMul IsScalarTower.right SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction mulActionBaseChange TensorProduct.zero	—	SMulCommClass.of_commMonoid IsScalarTower.right TensorProduct.zero_tmul Algebra.to_smulCommClass mulActionBaseChange_smul_tmul smul_zero
tensorKaehlerEquivBase_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids KaehlerDifferential TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential Algebra.toModule module' SMulCommClass.of_commMonoid CommRing.toCommMonoid Algebra.toSMul IsScalarTower.right TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm tensorKaehlerEquivBase LinearMap TensorProduct.addCommGroup Ring.toAddCommGroup CommRing.toRing Algebra.id moduleBaseChange' LinearMap.instFunLike Derivation.liftKaehlerDifferential instIsScalarTowerTensorProduct_2 derivationTensorProduct	—	RingHomInvPair.ids SMulCommClass.of_commMonoid IsScalarTower.right Algebra.to_smulCommClass
tensorKaehlerEquivBase_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct KaehlerDifferential NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential Algebra.toModule module' SMulCommClass.of_commMonoid CommRing.toCommMonoid Algebra.toSMul IsScalarTower.right TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv tensorKaehlerEquivBase TensorProduct.tmul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction LinearMap Algebra.id LinearMap.instFunLike map	—	LinearMap.liftBaseChange_tmul SMulCommClass.of_commMonoid IsScalarTower.right
tensorKaehlerEquiv_left_inv 📖	mathematical	—	LinearMap.comp TensorProduct CommRing.toCommSemiring KaehlerDifferential NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential Algebra.toModule module' SMulCommClass.of_commMonoid CommRing.toCommMonoid Algebra.toSMul IsScalarTower.right NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing TensorProduct.addCommMonoid TensorProduct.addCommGroup Ring.toAddCommGroup CommRing.toRing TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass RingHom.id RingHomCompTriple.ids LinearMap.restrictScalars Algebra.id moduleBaseChange' LinearMap.IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction isScalarTower_of_tower instIsScalarTowerTensorProduct_2 Derivation.liftKaehlerDifferential derivationTensorProduct LinearMap.liftBaseChange map LinearMap.id	—	LinearMap.restrictScalars_injective SMulCommClass.of_commMonoid IsScalarTower.right Algebra.to_smulCommClass LinearMap.IsScalarTower.compatibleSMul TensorProduct.isScalarTower_left RingHomCompTriple.ids isScalarTower_of_tower instIsScalarTowerTensorProduct_2 TensorProduct.ext' smulCommClass_self tensorProductTo_surjective TensorProduct.induction_on map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass TensorProduct.tmul_zero map_smul SemilinearMapClass.toMulActionSemiHomClass map_D LinearMap.map_smul_of_tower instIsScalarTowerTensorProduct_1 Derivation.liftKaehlerDifferential_comp_D derivationTensorProduct_algebraMap SMulCommClass.smul_comm instSMulCommClassTensorProduct TensorProduct.smul_tmul' smul_eq_mul mul_one map_add SemilinearMapClass.toAddHomClass TensorProduct.tmul_add
tensorKaehlerEquiv_symm_D_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule CommSemiring.toSemiring Algebra.TensorProduct.instCommRing RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids KaehlerDifferential Algebra.TensorProduct.leftAlgebra Algebra.id Algebra.to_smulCommClass AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential Algebra.TensorProduct.rightAlgebra module' TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm tensorKaehlerEquiv Algebra.TensorProduct.instAlgebra Algebra.TensorProduct.right_isScalarTower TensorProduct.isScalarTower_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toSMul IsScalarTower.right TensorProduct.isPushout Derivation smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing Derivation.instFunLike D TensorProduct.tmul RingHom Algebra.TensorProduct.instSemiring RingHom.instFunLike algebraMap	—	Algebra.to_smulCommClass RingHomInvPair.ids Algebra.TensorProduct.right_isScalarTower TensorProduct.isScalarTower_left IsScalarTower.right TensorProduct.isPushout smulCommClass_self LinearEquiv.symm_apply_eq tensorKaehlerEquiv_tmul_D Algebra.TensorProduct.right_algebraMap_apply TensorProduct.smulCommClass_left algebraMap_smul isScalarTower_of_tower Derivation.map_smul TensorProduct.smul_tmul' smul_eq_mul mul_one
tensorKaehlerEquiv_symm_D_tmul' 📖	mathematical	—	DFunLike.coe LinearEquiv TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule CommSemiring.toSemiring Algebra.TensorProduct.instCommRing RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids KaehlerDifferential Algebra.TensorProduct.rightAlgebra AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential Algebra.TensorProduct.leftAlgebra Algebra.id Algebra.to_smulCommClass module' TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm tensorKaehlerEquiv Algebra.TensorProduct.instAlgebra TensorProduct.isScalarTower_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toSMul IsScalarTower.right Algebra.TensorProduct.right_isScalarTower TensorProduct.isPushout' Derivation smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing Derivation.instFunLike D TensorProduct.tmul RingHom Algebra.TensorProduct.instSemiring RingHom.instFunLike algebraMap	—	Algebra.to_smulCommClass RingHomInvPair.ids TensorProduct.isScalarTower_left IsScalarTower.right Algebra.TensorProduct.right_isScalarTower TensorProduct.isPushout' smulCommClass_self LinearEquiv.symm_apply_eq tensorKaehlerEquiv_tmul_D SMulCommClass.of_commMonoid algebraMap_smul isScalarTower_of_tower Derivation.map_smul Algebra.smul_def Algebra.TensorProduct.right_algebraMap_apply one_mul mul_one
tensorKaehlerEquiv_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct KaehlerDifferential NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential Algebra.toModule module' SMulCommClass.of_commMonoid CommRing.toCommMonoid Algebra.toSMul IsScalarTower.right TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv tensorKaehlerEquivBase TensorProduct.tmul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction LinearMap Algebra.id LinearMap.instFunLike map	—	tensorKaehlerEquivBase_tmul
tensorKaehlerEquiv_tmul_D 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct KaehlerDifferential NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential Algebra.toModule module' Algebra.id Algebra.to_smulCommClass TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv tensorKaehlerEquiv TensorProduct.tmul Derivation smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Derivation.instFunLike D SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom RingHom.instFunLike algebraMap	—	Algebra.IsPushout.symm Algebra.to_smulCommClass RingHomInvPair.ids smulCommClass_self AlgEquiv.surjective TensorProduct.induction_on map_zero MonoidWithZeroHomClass.toZeroHomClass IsScalarTower.right RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass TensorProduct.zero_tmul AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass zero_smul SMulCommClass.of_commMonoid AlgEquiv.symm_apply_apply tensorKaehlerEquivBase_tmul map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass map_D Algebra.IsPushout.equiv_tmul SemigroupAction.mul_smul algebraMap_smul isScalarTower_of_tower SMulCommClass.smul_comm IsScalarTower.to_smulCommClass' map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass TensorProduct.add_tmul add_smul

---

← Back to Index