Documentation Verification Report

Kaehler

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

Statistics

Metric	Count
Definitions `derivationOfSectionOfKerSqZero`, `derivationQuotKerSq`, `retractionKerCotangentToTensorEquivSection`, `retractionKerToTensorEquivSection`, `retractionOfSectionOfKerSqZero`, `sectionOfRetractionKerToTensor`, `sectionOfRetractionKerToTensorAux`, `tensorKaehlerQuotKerSqEquiv`	8
Theorems `map_toInfinitesimal_bijective`, `map_toInfinitesimal_bijective`, `map_toInfinitesimal_bijective`, `derivationOfSectionOfKerSqZero_apply_coe`, `derivationQuotKerSq_mk`, `isScalarTower_of_section_of_ker_sqZero`, `retractionOfSectionOfKerSqZero_comp_kerToTensor`, `retractionOfSectionOfKerSqZero_tmul_D`, `sectionOfRetractionKerToTensorAux_algebraMap`, `sectionOfRetractionKerToTensorAux_prop`, `sectionOfRetractionKerToTensor_algebraMap`, `tensorKaehlerQuotKerSqEquiv_symm_tmul_D`, `tensorKaehlerQuotKerSqEquiv_tmul_D`, `toAlgHom_comp_sectionOfRetractionKerToTensor`, `toAlgHom_comp_sectionOfRetractionKerToTensorAux`	15
Total	23

Algebra.Extension.Cotangent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_toInfinitesimal_bijective` 📖	mathematical	—	`Function.Bijective` `Algebra.Extension.Cotangent` `Algebra.Extension.infinitesimal` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Algebra.Extension.instAddCommGroupCotangent` `Algebra.Extension.instModuleCotangent` `Algebra.id` `LinearMap.instFunLike` `map` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Algebra.toModule` `Algebra.Extension.toInfinitesimal`	—	`IsScalarTower.left` `injective_iff_map_eq_zero` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `mk_surjective` `Ideal.cotangentIdeal_square` `Algebra.Extension.ker_infinitesimal` `ext` `Ideal.instIsTwoSided_1` `Ideal.Quotient.mk_surjective` `Ideal.mk_mem_cotangentIdeal`

Algebra.Extension.CotangentSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_toInfinitesimal_bijective` 📖	mathematical	—	`Function.Bijective` `Algebra.Extension.CotangentSpace` `Algebra.Extension.infinitesimal` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct.addCommMonoid` `Algebra.Extension.Ring` `Algebra.Extension.commRing` `KaehlerDifferential` `Algebra.Extension.instRingOfIsScalarTower` `Algebra.id` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Algebra.toModule` `Algebra.Extension.algebra₂` `KaehlerDifferential.module'` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `SMulCommClass.of_commMonoid` `CommRing.toCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsScalarTower.right` `LinearMap.instFunLike` `map` `IsScalarTower.left` `DistribMulAction.toMulAction` `Algebra.Extension.toInfinitesimal`	—	`Algebra.to_smulCommClass` `SMulCommClass.of_commMonoid` `IsScalarTower.right` `IsScalarTower.left` `RingHomInvPair.ids` `RingHom.instRingHomClass` `Algebra.Extension.instIsScalarTowerRing_2` `IsScalarTower.of_algebraMap_eq'` `LinearMap.restrictScalars_injective` `IsScalarTower.to_smulCommClass'` `LinearMap.IsScalarTower.compatibleSMul` `TensorProduct.isScalarTower_left` `TensorProduct.AlgebraTensorModule.curry_injective` `TensorProduct.isScalarTower_right` `instSMulCommClass` `TensorProduct.CompatibleSMul.isScalarTower` `KaehlerDifferential.isScalarTower_of_tower` `LinearMap.ext` `IsScalarTower.to_smulCommClass` `Derivation.liftKaehlerDifferential_unique` `Derivation.ext` `smulCommClass_self` `map_tmul` `Ideal.instIsTwoSided_1` `tensorKaehlerQuotKerSqEquiv_symm_tmul_D` `LinearEquiv.bijective`

Algebra.Extension.H1Cotangent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_toInfinitesimal_bijective` 📖	mathematical	—	`Function.Bijective` `Algebra.Extension.H1Cotangent` `Algebra.Extension.infinitesimal` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Algebra.Extension.instAddCommGroupH1Cotangent` `Algebra.Extension.instModuleH1CotangentOfIsScalarTowerCotangent` `Algebra.id` `Algebra.Extension.instModuleCotangent` `Algebra.Extension.instIsScalarTowerCotangent` `IsScalarTower.right` `LinearMap.instFunLike` `map` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Algebra.toModule` `Algebra.Extension.toInfinitesimal`	—	`Algebra.Extension.instIsScalarTowerCotangent` `IsScalarTower.right` `IsScalarTower.left` `Algebra.Extension.h1Cotangentι_ext` `Algebra.Extension.Cotangent.map_toInfinitesimal_bijective` `Algebra.to_smulCommClass` `SMulCommClass.of_commMonoid` `map_eq_zero_iff` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Function.Bijective.injective` `Algebra.Extension.CotangentSpace.map_toInfinitesimal_bijective`

(root)

Definitions

Name	Category	Theorems
`derivationOfSectionOfKerSqZero` 📖	CompOp	1 math math: `derivationOfSectionOfKerSqZero_apply_coe`
`derivationQuotKerSq` 📖	CompOp	1 math math: `derivationQuotKerSq_mk`
`retractionKerCotangentToTensorEquivSection` 📖	CompOp	—
`retractionKerToTensorEquivSection` 📖	CompOp	—
`retractionOfSectionOfKerSqZero` 📖	CompOp	2 math math: `retractionOfSectionOfKerSqZero_comp_kerToTensor`, `retractionOfSectionOfKerSqZero_tmul_D`
`sectionOfRetractionKerToTensor` 📖	CompOp	2 math math: `sectionOfRetractionKerToTensor_algebraMap`, `toAlgHom_comp_sectionOfRetractionKerToTensor`
`sectionOfRetractionKerToTensorAux` 📖	CompOp	2 math math: `toAlgHom_comp_sectionOfRetractionKerToTensorAux`, `sectionOfRetractionKerToTensorAux_algebraMap`
`tensorKaehlerQuotKerSqEquiv` 📖	CompOp	2 math math: `tensorKaehlerQuotKerSqEquiv_symm_tmul_D`, `tensorKaehlerQuotKerSqEquiv_tmul_D`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`derivationOfSectionOfKerSqZero_apply_coe` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `RingHom.ker` `AlgHom` `AlgHom.funLike` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Bot.bot` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `AlgHom.comp` `AlgHom.id`	`SetLike.instMembership` `Submodule.setLike` `DFunLike.coe` `Derivation` `Submodule.addCommMonoid` `Submodule.module` `Submodule.module'` `Algebra.toSMul` `Algebra.toModule` `IsScalarTower.right` `Derivation.instFunLike` `derivationOfSectionOfKerSqZero` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `IsScalarTower.right`
`derivationQuotKerSq_mk` 📖	mathematical	—	`DFunLike.coe` `Derivation` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `RingHom.ker` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `RingHom.instRingHomClass` `algebraMap` `TensorProduct` `KaehlerDifferential` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Algebra.toModule` `KaehlerDifferential.module'` `Algebra.to_smulCommClass` `Ideal.Quotient.commSemiring` `TensorProduct.addCommMonoid` `Ideal.instAlgebraQuotient` `TensorProduct.leftModule` `Ideal.Algebra.kerSquareLift` `IsScalarTower.to_smulCommClass` `Ideal.instIsScalarTowerQuotientHPowKerRingHomAlgebraMapOfNat` `IsScalarTower.left` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `IsScalarTower.to_smulCommClass'` `Derivation.instFunLike` `derivationQuotKerSq` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `TensorProduct.tmul` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `smulCommClass_self` `CommRing.toCommMonoid` `CommMonoid.toMonoid` `KaehlerDifferential.D`	—	`Algebra.to_smulCommClass` `RingHom.instRingHomClass` `IsScalarTower.to_smulCommClass` `Ideal.instIsScalarTowerQuotientHPowKerRingHomAlgebraMapOfNat` `IsScalarTower.left` `IsScalarTower.to_smulCommClass'` `Ideal.instIsTwoSided_1`
`isScalarTower_of_section_of_ker_sqZero` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `RingHom.ker` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `RingHom.instRingHomClass` `algebraMap` `Bot.bot` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `AlgHom.comp` `IsScalarTower.toAlgHom` `AlgHom.id`	`IsScalarTower` `SetLike.instMembership` `Submodule.setLike` `Algebra.toSMul` `Submodule.smul` `RingHom.toAlgebra` `AlgHom.toRingHom` `IsScalarTower.right`	—	`RingHom.instRingHomClass` `IsScalarTower.right` `Algebra.smul_def` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `mul_assoc` `mul_left_comm` `sub_eq_zero` `Ideal.mem_bot` `pow_two` `sub_mul` `Ideal.mul_mem_mul` `map_sub` `RingHomClass.toAddMonoidHomClass` `AlgHom.congr_fun`
`retractionOfSectionOfKerSqZero_comp_kerToTensor` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `RingHom.ker` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `RingHom.instRingHomClass` `algebraMap` `Bot.bot` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `AlgHom.comp` `IsScalarTower.toAlgHom` `AlgHom.id`	`LinearMap.comp` `SetLike.instMembership` `Submodule.setLike` `TensorProduct` `KaehlerDifferential` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Algebra.toModule` `KaehlerDifferential.module'` `Algebra.to_smulCommClass` `Submodule.addCommMonoid` `TensorProduct.addCommMonoid` `Submodule.module` `TensorProduct.instModule` `RingHom.id` `RingHomCompTriple.ids` `retractionOfSectionOfKerSqZero` `KaehlerDifferential.kerToTensor` `LinearMap.id`	—	`RingHom.instRingHomClass` `LinearMap.ext` `Algebra.to_smulCommClass` `RingHomCompTriple.ids` `smulCommClass_self` `retractionOfSectionOfKerSqZero_tmul_D` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `one_mul` `RingHom.mem_ker` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `MulZeroClass.mul_zero` `sub_zero`
`retractionOfSectionOfKerSqZero_tmul_D` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `RingHom.ker` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `RingHom.instRingHomClass` `algebraMap` `Bot.bot` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `AlgHom.comp` `IsScalarTower.toAlgHom` `AlgHom.id`	`SetLike.instMembership` `Submodule.setLike` `DFunLike.coe` `LinearMap` `RingHom.id` `TensorProduct` `KaehlerDifferential` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Algebra.toModule` `KaehlerDifferential.module'` `Algebra.to_smulCommClass` `TensorProduct.addCommMonoid` `Submodule.addCommMonoid` `TensorProduct.instModule` `Submodule.module` `LinearMap.instFunLike` `retractionOfSectionOfKerSqZero` `TensorProduct.tmul` `Derivation` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Derivation.instFunLike` `KaehlerDifferential.D` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AlgHom` `AlgHom.funLike`	—	`RingHom.instRingHomClass` `Algebra.to_smulCommClass` `smulCommClass_self` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Derivation.liftKaehlerDifferential_comp_D` `mul_sub`
`sectionOfRetractionKerToTensorAux_algebraMap` 📖	mathematical	`LinearMap.comp` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.ker` `RingHom` `RingHom.instFunLike` `RingHom.instRingHomClass` `algebraMap` `TensorProduct` `KaehlerDifferential` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Algebra.toModule` `KaehlerDifferential.module'` `Algebra.id` `Algebra.to_smulCommClass` `Submodule.addCommMonoid` `TensorProduct.addCommMonoid` `Submodule.module` `TensorProduct.instModule` `RingHom.id` `RingHomCompTriple.ids` `KaehlerDifferential.kerToTensor` `LinearMap.id` `DFunLike.coe` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Bot.bot` `Submodule.instBot`	`AlgHom` `AlgHom.funLike` `sectionOfRetractionKerToTensorAux` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `LinearMap` `LinearMap.instFunLike` `TensorProduct.tmul` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Derivation` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `Derivation.instFunLike` `KaehlerDifferential.D`	—	`Algebra.to_smulCommClass` `RingHom.instRingHomClass` `RingHomCompTriple.ids` `sectionOfRetractionKerToTensorAux_prop`
`sectionOfRetractionKerToTensorAux_prop` 📖	mathematical	`LinearMap.comp` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.ker` `RingHom` `RingHom.instFunLike` `RingHom.instRingHomClass` `algebraMap` `TensorProduct` `KaehlerDifferential` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Algebra.toModule` `KaehlerDifferential.module'` `Algebra.id` `Algebra.to_smulCommClass` `Submodule.addCommMonoid` `TensorProduct.addCommMonoid` `Submodule.module` `TensorProduct.instModule` `RingHom.id` `RingHomCompTriple.ids` `KaehlerDifferential.kerToTensor` `LinearMap.id` `DFunLike.coe`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `LinearMap` `LinearMap.instFunLike` `TensorProduct.tmul` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Derivation` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `Derivation.instFunLike` `KaehlerDifferential.D`	—	`Algebra.to_smulCommClass` `RingHom.instRingHomClass` `RingHomCompTriple.ids` `smulCommClass_self` `sub_eq_iff_eq_add` `sub_add_comm` `Submodule.addSubgroupClass` `Submodule.coe_sub` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `TensorProduct.tmul_sub` `Derivation.instAddMonoidHomClass` `RingHomClass.toAddMonoidHomClass` `sub_self` `LinearMap.congr_fun`
`sectionOfRetractionKerToTensor_algebraMap` 📖	mathematical	`LinearMap.comp` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.ker` `RingHom` `RingHom.instFunLike` `RingHom.instRingHomClass` `algebraMap` `TensorProduct` `KaehlerDifferential` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Algebra.toModule` `KaehlerDifferential.module'` `Algebra.id` `Algebra.to_smulCommClass` `Submodule.addCommMonoid` `TensorProduct.addCommMonoid` `Submodule.module` `TensorProduct.instModule` `RingHom.id` `RingHomCompTriple.ids` `KaehlerDifferential.kerToTensor` `LinearMap.id` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Bot.bot` `Submodule.instBot` `DFunLike.coe`	`AlgHom` `AlgHom.funLike` `sectionOfRetractionKerToTensor` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `LinearMap` `LinearMap.instFunLike` `TensorProduct.tmul` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Derivation` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `Derivation.instFunLike` `KaehlerDifferential.D`	—	`Algebra.to_smulCommClass` `RingHom.instRingHomClass` `RingHomCompTriple.ids` `sectionOfRetractionKerToTensorAux_algebraMap`
`tensorKaehlerQuotKerSqEquiv_symm_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` `KaehlerDifferential.module'` `Algebra.id` `Algebra.to_smulCommClass` `HasQuotient.Quotient` `Ideal` `Ideal.instHasQuotient_1` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `RingHom.ker` `RingHom` `RingHom.instFunLike` `RingHom.instRingHomClass` `algebraMap` `Ideal.Quotient.commSemiring` `Ideal.Quotient.commRing` `Ideal.instAlgebraQuotient` `Ideal.Algebra.kerSquareLift` `Ideal.Quotient.semiring` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `tensorKaehlerQuotKerSqEquiv` `TensorProduct.tmul` `Derivation` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Derivation.instFunLike` `KaehlerDifferential.D` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1`	—	`LinearEquiv.injective` `RingHom.instRingHomClass` `Algebra.to_smulCommClass` `RingHomInvPair.ids` `smulCommClass_self` `Ideal.instIsTwoSided_1` `LinearEquiv.apply_symm_apply` `tensorKaehlerQuotKerSqEquiv_tmul_D`
`tensorKaehlerQuotKerSqEquiv_tmul_D` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `HasQuotient.Quotient` `Ideal` `Ideal.instHasQuotient_1` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `RingHom.ker` `RingHom` `RingHom.instFunLike` `RingHom.instRingHomClass` `algebraMap` `Ideal.Quotient.commSemiring` `KaehlerDifferential` `Ideal.Quotient.commRing` `Ideal.instAlgebraQuotient` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Algebra.toModule` `Ideal.Algebra.kerSquareLift` `KaehlerDifferential.module'` `Algebra.to_smulCommClass` `Ideal.Quotient.semiring` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `tensorKaehlerQuotKerSqEquiv` `TensorProduct.tmul` `Derivation` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Derivation.instFunLike` `KaehlerDifferential.D` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1`	—	`Algebra.to_smulCommClass` `RingHomInvPair.ids` `RingHom.instRingHomClass` `smulCommClass_self` `Ideal.instIsTwoSided_1` `IsScalarTower.to_smulCommClass` `Ideal.instIsScalarTowerQuotientHPowKerRingHomAlgebraMapOfNat` `IsScalarTower.left` `IsScalarTower.to_smulCommClass'` `TensorProduct.isScalarTower_left` `Derivation.liftKaehlerDifferential_comp_D` `mul_one`
`toAlgHom_comp_sectionOfRetractionKerToTensor` 📖	mathematical	`LinearMap.comp` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.ker` `RingHom` `RingHom.instFunLike` `RingHom.instRingHomClass` `algebraMap` `TensorProduct` `KaehlerDifferential` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Algebra.toModule` `KaehlerDifferential.module'` `Algebra.id` `Algebra.to_smulCommClass` `Submodule.addCommMonoid` `TensorProduct.addCommMonoid` `Submodule.module` `TensorProduct.instModule` `RingHom.id` `RingHomCompTriple.ids` `KaehlerDifferential.kerToTensor` `LinearMap.id` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Bot.bot` `Submodule.instBot` `DFunLike.coe`	`AlgHom.comp` `IsScalarTower.toAlgHom` `sectionOfRetractionKerToTensor` `AlgHom.id`	—	`Algebra.to_smulCommClass` `RingHom.instRingHomClass` `RingHomCompTriple.ids` `toAlgHom_comp_sectionOfRetractionKerToTensorAux`
`toAlgHom_comp_sectionOfRetractionKerToTensorAux` 📖	mathematical	`LinearMap.comp` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.ker` `RingHom` `RingHom.instFunLike` `RingHom.instRingHomClass` `algebraMap` `TensorProduct` `KaehlerDifferential` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `instAddCommGroupKaehlerDifferential` `Algebra.toModule` `KaehlerDifferential.module'` `Algebra.id` `Algebra.to_smulCommClass` `Submodule.addCommMonoid` `TensorProduct.addCommMonoid` `Submodule.module` `TensorProduct.instModule` `RingHom.id` `RingHomCompTriple.ids` `KaehlerDifferential.kerToTensor` `LinearMap.id` `DFunLike.coe` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Bot.bot` `Submodule.instBot`	`AlgHom.comp` `IsScalarTower.toAlgHom` `sectionOfRetractionKerToTensorAux` `AlgHom.id`	—	`Algebra.to_smulCommClass` `RingHom.instRingHomClass` `RingHomCompTriple.ids` `AlgHom.ext` `smulCommClass_self` `sectionOfRetractionKerToTensorAux_algebraMap` `map_sub` `RingHomClass.toAddMonoidHomClass` `RingHom.mem_ker` `sub_zero`

---

← Back to Index