Basic

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

Statistics

Metric	Count
Definitions liftKaehlerDifferential, tensorProductTo, KaehlerDifferential, D, DLinearMap, derivationQuotKerTotal, endEquiv, endEquivAuxEquiv, endEquivDerivation', fromIdeal, ideal, kerCotangentToTensor, kerToTensor, kerTotal, linearMapEquivDerivation, map, mapBaseChange, module', quotKerTotalEquiv, quotientCotangentIdeal, quotientCotangentIdealRingEquiv, instAddCommGroupKaehlerDifferential, instInhabitedKaehlerDifferential, instIsScalarTowerTensorProductKaehlerDifferential, instModuleTensorProductKaehlerDifferential, instR, «termΩ[_⁄_]»	27
Theorems liftKaehlerDifferential_D, liftKaehlerDifferential_apply, liftKaehlerDifferential_comp, liftKaehlerDifferential_comp_D, liftKaehlerDifferential_unique, liftKaehlerDifferential_unique_iff, tensorProductTo_mul, tensorProductTo_tmul, DLinearMap_apply, D_apply, D_tensorProductTo, End_equiv_aux, derivationQuotKerTotal_apply, derivationQuotKerTotal_lift_comp_linearCombination, exact_kerCotangentToTensor_mapBaseChange, exact_mapBaseChange_map, finite, ideal_fg, isScalarTower', isScalarTower_of_tower, kerCotangentToTensor_toCotangent, kerToTensor_apply, kerTotal_eq, kerTotal_map, kerTotal_map', kerTotal_mkQ_single_add, kerTotal_mkQ_single_algebraMap, kerTotal_mkQ_single_algebraMap_one, kerTotal_mkQ_single_mul, kerTotal_mkQ_single_smul, ker_map, ker_map_of_surjective, linearCombination_surjective, linearMapEquivDerivation_apply_apply, linearMapEquivDerivation_symm_apply, mapBaseChange_surjective, mapBaseChange_tmul, map_D, map_compDer, map_surjective, map_surjective_of_surjective, one_smul_sub_smul_one_mem_ideal, quotKerTotalEquiv_apply, quotKerTotalEquiv_symm_apply, quotKerTotalEquiv_symm_comp_D, range_kerCotangentToTensor, range_mapBaseChange, span_range_derivation, span_range_eq_ideal, submodule_span_range_eq_ideal, subsingleton_of_surjective, tensorProductTo_surjective	52
Total	79

Derivation

Definitions

Name	Category	Theorems
liftKaehlerDifferential 📖	CompOp	9 math math: KaehlerDifferential.tensorKaehlerEquivBase_symm_apply, KaehlerDifferential.linearMapEquivDerivation_symm_apply, liftKaehlerDifferential_comp, liftKaehlerDifferential_comp_D, KaehlerDifferential.tensorKaehlerEquiv_left_inv, liftKaehlerDifferential_D, KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination, KaehlerDifferential.quotKerTotalEquiv_symm_apply, liftKaehlerDifferential_apply
tensorProductTo 📖	CompOp	5 math math: KaehlerDifferential.D_tensorProductTo, tensorProductTo_mul, KaehlerDifferential.tensorProductTo_surjective, tensorProductTo_tmul, liftKaehlerDifferential_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
liftKaehlerDifferential_D 📖	mathematical	—	liftKaehlerDifferential KaehlerDifferential instAddCommGroupKaehlerDifferential KaehlerDifferential.module' smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toModule CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id Algebra.to_smulCommClass KaehlerDifferential.isScalarTower_of_tower Algebra.toSMul IsScalarTower.right KaehlerDifferential.D LinearMap.id AddCommGroup.toAddCommMonoid	—	liftKaehlerDifferential_unique smulCommClass_self Algebra.to_smulCommClass KaehlerDifferential.isScalarTower_of_tower IsScalarTower.right liftKaehlerDifferential_comp
liftKaehlerDifferential_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring KaehlerDifferential AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential KaehlerDifferential.module' Algebra.id Algebra.to_smulCommClass LinearMap.instFunLike liftKaehlerDifferential TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Algebra.TensorProduct.instCommRing Ideal SetLike.instMembership Submodule.setLike NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule KaehlerDifferential.ideal Ideal.Cotangent Submodule.addCommMonoid Ideal.instAddCommGroupCotangent Submodule.module Ideal.instModuleCotangentOfAlgebra Ideal.toCotangent TensorProduct.addCommMonoid TensorProduct.leftModule tensorProductTo	—	Algebra.to_smulCommClass
liftKaehlerDifferential_comp 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Derivation KaehlerDifferential AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential KaehlerDifferential.module' Algebra.id Algebra.to_smulCommClass smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toModule instAddCommMonoid instModule IsScalarTower.to_smulCommClass KaehlerDifferential.isScalarTower_of_tower Algebra.toSMul IsScalarTower.right CommSemiring.toCommMonoid LinearMap.instFunLike LinearMap.compDer liftKaehlerDifferential KaehlerDifferential.D	—	ext Algebra.to_smulCommClass smulCommClass_self IsScalarTower.to_smulCommClass KaehlerDifferential.isScalarTower_of_tower IsScalarTower.right KaehlerDifferential.one_smul_sub_smul_one_mem_ideal liftKaehlerDifferential_apply map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass tensorProductTo_tmul one_smul map_one_eq_zero smul_zero sub_zero
liftKaehlerDifferential_comp_D 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring KaehlerDifferential AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential KaehlerDifferential.module' Algebra.id Algebra.to_smulCommClass LinearMap.instFunLike liftKaehlerDifferential Derivation smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toModule instFunLike KaehlerDifferential.D	—	congr_fun Algebra.to_smulCommClass smulCommClass_self IsScalarTower.to_smulCommClass KaehlerDifferential.isScalarTower_of_tower IsScalarTower.right liftKaehlerDifferential_comp
liftKaehlerDifferential_unique 📖	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Derivation KaehlerDifferential AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential KaehlerDifferential.module' Algebra.id Algebra.to_smulCommClass smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toModule instAddCommMonoid instModule IsScalarTower.to_smulCommClass KaehlerDifferential.isScalarTower_of_tower Algebra.toSMul IsScalarTower.right CommSemiring.toCommMonoid LinearMap.instFunLike LinearMap.compDer KaehlerDifferential.D	—	—	Algebra.to_smulCommClass smulCommClass_self IsScalarTower.to_smulCommClass KaehlerDifferential.isScalarTower_of_tower IsScalarTower.right LinearMap.ext KaehlerDifferential.span_range_derivation Submodule.span_induction map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass map_add SemilinearMapClass.toAddHomClass map_smul SemilinearMapClass.toMulActionSemiHomClass
liftKaehlerDifferential_unique_iff 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Derivation KaehlerDifferential AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential KaehlerDifferential.module' Algebra.id Algebra.to_smulCommClass smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toModule instAddCommMonoid instModule IsScalarTower.to_smulCommClass KaehlerDifferential.isScalarTower_of_tower Algebra.toSMul IsScalarTower.right CommSemiring.toCommMonoid LinearMap.instFunLike LinearMap.compDer KaehlerDifferential.D	—	Algebra.to_smulCommClass smulCommClass_self IsScalarTower.to_smulCommClass KaehlerDifferential.isScalarTower_of_tower IsScalarTower.right liftKaehlerDifferential_unique
tensorProductTo_mul 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule TensorProduct.addCommMonoid AddCommGroup.toAddCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass LinearMap.instFunLike tensorProductTo Algebra.TensorProduct.instMul IsScalarTower.right AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AlgHom NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.TensorProduct.instSemiring Algebra.TensorProduct.instAlgebra AlgHom.funLike Algebra.TensorProduct.lmul'	—	TensorProduct.induction_on Algebra.to_smulCommClass IsScalarTower.right MulZeroClass.zero_mul map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass zero_smul smul_zero add_zero MulZeroClass.mul_zero smulCommClass_self IsScalarTower.to_smulCommClass LinearMap.IsScalarTower.compatibleSMul LinearMap.instIsScalarTower leibniz smul_add smul_smul mul_right_comm mul_comm mul_add Distrib.leftDistribClass map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass add_smul add_add_add_comm add_mul Distrib.rightDistribClass
tensorProductTo_tmul 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule TensorProduct.addCommMonoid AddCommGroup.toAddCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass LinearMap.instFunLike tensorProductTo 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 Derivation instFunLike	—	Algebra.to_smulCommClass

KaehlerDifferential

Definitions

Name	Category	Theorems
D 📖	CompOp	60 math math: kerCotangentToTensor_toCotangent, mvPolynomialBasis_apply, polynomialEquiv_symm, tensorKaehlerEquiv_symm_D_tmul', Algebra.Generators.cotangentSpaceBasis_apply, mvPolynomialBasis_repr_D_X, tensorKaehlerEquiv_symm_D_tmul, polynomialEquiv_D, kerToTensor_apply, quotKerTotalEquiv_symm_comp_D, Algebra.Generators.cotangentSpaceBasis_repr_one_tmul, Algebra.SubmersivePresentation.basisKaehlerOfIsCompl_apply, kerTotal_eq, Algebra.Generators.H1Cotangent.δAux_C, Algebra.Extension.CotangentSpace.map_tmul, polynomialEquiv_comp_D, span_range_map_derivation_of_isLocalization, linearMapEquivDerivation_apply_apply, span_range_derivation, Algebra.Generators.H1Cotangent.δAux_monomial, Algebra.Generators.cotangentSpaceBasis_repr_tmul, Algebra.Extension.Hom.sub_one_tmul, Algebra.Generators.H1Cotangent.δAux_toAlgHom, D_apply, Derivation.liftKaehlerDifferential_comp, ker_map, tensorKaehlerQuotKerSqEquiv_symm_tmul_D, Derivation.liftKaehlerDifferential_comp_D, Algebra.Generators.H1Cotangent.δAux_ofComp, Algebra.Presentation.differentials.comm₂₃', sectionOfRetractionKerToTensorAux_prop, Derivation.liftKaehlerDifferential_unique_iff, Derivation.liftKaehlerDifferential_D, tensorKaehlerQuotKerSqEquiv_tmul_D, mvPolynomialBasis_repr_apply, Algebra.Generators.toKaehler_tmul_D, sectionOfRetractionKerToTensor_algebraMap, map_compDer, D_tensorProductTo, derivationQuotKerTotal_lift_comp_linearCombination, Algebra.Generators.toKaehler_cotangentSpaceBasis, Algebra.SubmersivePresentation.basisKaehler_apply, polynomial_D_apply, derivationTensorProduct_algebraMap, tensorProductTo_surjective, sectionOfRetractionKerToTensorAux_algebraMap, mvPolynomialBasis_repr_D, ker_map_of_surjective, tensorKaehlerEquivOfFormallyEtale_symm_D_algebraMap, mvPolynomialBasis_repr_comp_D, Algebra.Extension.Hom.sub_tmul, mvPolynomialBasis_repr_symm_single, Algebra.IsStandardSmooth.iff_exists_basis_kaehlerDifferential, map_D, tensorKaehlerEquiv_tmul_D, quotKerTotalEquiv_apply, Algebra.Extension.cotangentComplex_mk, retractionOfSectionOfKerSqZero_tmul_D, linearCombination_surjective, derivationQuotKerSq_mk
DLinearMap 📖	CompOp	1 math math: DLinearMap_apply
derivationQuotKerTotal 📖	CompOp	4 math math: quotKerTotalEquiv_symm_comp_D, derivationQuotKerTotal_apply, derivationQuotKerTotal_lift_comp_linearCombination, quotKerTotalEquiv_symm_apply
endEquiv 📖	CompOp	—
endEquivAuxEquiv 📖	CompOp	—
endEquivDerivation' 📖	CompOp	—
fromIdeal 📖	CompOp	—
ideal 📖	CompOp	9 math math: ideal_fg, End_equiv_aux, D_apply, one_smul_sub_smul_one_mem_ideal, submodule_span_range_eq_ideal, D_tensorProductTo, span_range_eq_ideal, Derivation.liftKaehlerDifferential_apply, DLinearMap_apply
kerCotangentToTensor 📖	CompOp	5 math math: kerCotangentToTensor_toCotangent, exact_kerCotangentToTensor_mapBaseChange, Algebra.FormallySmooth.kerCotangentToTensor_injective_iff, range_kerCotangentToTensor, Algebra.FormallySmooth.iff_split_injection
kerToTensor 📖	CompOp	3 math math: cotangentComplexBaseChange_tmul, kerToTensor_apply, retractionOfSectionOfKerSqZero_comp_kerToTensor
kerTotal 📖	CompOp	14 math math: quotKerTotalEquiv_symm_comp_D, kerTotal_eq, kerTotal_mkQ_single_algebraMap_one, kerTotal_mkQ_single_add, ker_map, derivationQuotKerTotal_apply, kerTotal_map, kerTotal_mkQ_single_mul, derivationQuotKerTotal_lift_comp_linearCombination, kerTotal_mkQ_single_smul, quotKerTotalEquiv_symm_apply, quotKerTotalEquiv_apply, kerTotal_map', kerTotal_mkQ_single_algebraMap
linearMapEquivDerivation 📖	CompOp	2 math math: linearMapEquivDerivation_apply_apply, linearMapEquivDerivation_symm_apply
map 📖	CompOp	19 math math: isLocalizedModule_of_isLocalizedModule, mapBaseChange_tmul, span_range_map_derivation_of_isLocalization, tensorKaehlerEquivBase_tmul, isLocalizedModule_map, exact_mapBaseChange_map, tensorKaehlerEquiv_tmul, range_mapBaseChange, ker_map, map_surjective_of_surjective, tensorKaehlerEquiv_left_inv, isBaseChange, map_surjective, map_compDer, isLocalizedModule, ker_map_of_surjective, isBaseChange_of_formallyEtale, map_D, map_liftBaseChange_smul
mapBaseChange 📖	CompOp	9 math math: mapBaseChange_tmul, tensorKaehlerEquivOfFormallyEtale_apply, exact_mapBaseChange_map, range_mapBaseChange, Algebra.Generators.H1Cotangent.exact_δ_map, mapBaseChange_surjective, exact_kerCotangentToTensor_mapBaseChange, range_kerCotangentToTensor, Algebra.H1Cotangent.exact_δ_mapBaseChange
module' 📖	CompOp	162 math math: kerCotangentToTensor_toCotangent, mvPolynomialBasis_apply, Algebra.Presentation.differentials.comm₁₂_single, Algebra.Generators.H1Cotangent.δAux_mul, Algebra.Presentation.differentialsSolution_isPresentation, polynomialEquiv_symm, Algebra.Extension.H1Cotangent.equiv_apply, tensorKaehlerEquiv_symm_D_tmul', Algebra.Generators.cotangentSpaceBasis_apply, mvPolynomialBasis_repr_D_X, tensorKaehlerEquiv_symm_D_tmul, Algebra.FormallySmooth.projective_kaehlerDifferential, Algebra.Presentation.differentials.comm₂₃, cotangentComplexBaseChange_tmul, Algebra.Extension.formallySmooth_iff_split_injection, polynomialEquiv_D, Algebra.FormallySmooth.instFinitePresentationKaehlerDifferentialOfEssFiniteType, Algebra.Extension.CotangentSpace.map_id, kerToTensor_apply, isScalarTower', quotKerTotalEquiv_symm_comp_D, Algebra.Extension.lTensor_cotangentComplex_eq_cotangentComplexBaseChange, isLocalizedModule_of_isLocalizedModule, Algebra.Generators.cotangentSpaceBasis_repr_one_tmul, instIsScalarTowerTensorProduct, Algebra.SubmersivePresentation.basisKaehlerOfIsCompl_apply, retractionOfSectionOfKerSqZero_comp_kerToTensor, mapBaseChange_tmul, kerTotal_eq, Algebra.Generators.H1Cotangent.δAux_C, Algebra.FormallySmooth.iff_injective_cotangentComplexBaseChange_residueField, Algebra.Extension.subsingleton_h1Cotangent, Algebra.Extension.CotangentSpace.map_tmul, polynomialEquiv_comp_D, span_range_map_derivation_of_isLocalization, Algebra.Extension.H1Cotangent.val_zero, mulActionBaseChange_smul_add, Algebra.FormallySmooth.iff_injective_lTensor_residueField, Algebra.IsStandardSmoothOfRelativeDimension.iff_of_isStandardSmooth, linearMapEquivDerivation_apply_apply, tensorKaehlerEquivBase_tmul, Algebra.FormallySmooth.iff_subsingleton_and_projective, tensorKaehlerEquivBase_symm_apply, isLocalizedModule_map, isScalarTower_of_tower, tensorKaehlerEquivOfFormallyEtale_apply, linearMapEquivDerivation_symm_apply, span_range_derivation, Algebra.Generators.H1Cotangent.exact_map_δ, Algebra.Generators.H1Cotangent.δAux_monomial, Algebra.Generators.CotangentSpace.compEquiv_symm_zero, Algebra.Generators.cotangentSpaceBasis_repr_tmul, Algebra.Extension.Hom.sub_one_tmul, exact_mapBaseChange_map, tensorKaehlerEquiv_tmul, Algebra.Generators.H1Cotangent.δAux_toAlgHom, D_apply, Algebra.Extension.CotangentSpace.map_toInfinitesimal_bijective, range_mapBaseChange, Algebra.SubmersivePresentation.sectionCotangent_eq_iff, Algebra.Generators.H1Cotangent.exact_δ_map, Derivation.liftKaehlerDifferential_comp, ker_map, mapBaseChange_surjective, Algebra.Extension.CotangentSpace.map_sub_map, map_surjective_of_surjective, Algebra.unramifiedLocus_eq_compl_support, finite, Algebra.Extension.CotangentSpace.map_cotangentComplex, Algebra.Extension.cotangentComplexBaseChange_eq_lTensor_cotangentComplex, tensorKaehlerQuotKerSqEquiv_symm_tmul_D, Derivation.liftKaehlerDifferential_comp_D, Algebra.Generators.H1Cotangent.δAux_ofComp, Algebra.Presentation.differentials.comm₂₃', instSMulCommClassTensorProduct_1, tensorKaehlerEquiv_left_inv, Derivation.liftKaehlerDifferential_unique_iff, Derivation.liftKaehlerDifferential_D, tensorKaehlerQuotKerSqEquiv_tmul_D, isBaseChange, instSMulCommClassTensorProduct, mvPolynomialBasis_repr_apply, Algebra.Extension.h1Cotangentι_ext_iff, Algebra.Generators.toKaehler_tmul_D, exact_kerCotangentToTensor_mapBaseChange, Algebra.Extension.H1Cotangent.val_add, Algebra.Extension.H1Cotangent.val_smul, Algebra.Presentation.differentials.comm₁₂, map_surjective, map_compDer, Algebra.SubmersivePresentation.free_kaehlerDifferential, Algebra.Generators.H1Cotangent.exact_map_δ', D_tensorProductTo, Algebra.Extension.toKaehler_surjective, Algebra.Generators.CotangentSpace.exact, Algebra.Generators.H1Cotangent.δAux_X, derivationQuotKerTotal_lift_comp_linearCombination, Algebra.Generators.repr_CotangentSpaceMap, isLocalizedModule, Algebra.Extension.H1Cotangent.map_apply_coe, Algebra.Generators.toKaehler_cotangentSpaceBasis, Algebra.SubmersivePresentation.basisKaehler_apply, polynomial_D_apply, Algebra.Generators.CotangentSpace.compEquiv_symm_inr, quotKerTotalEquiv_symm_apply, Algebra.FormallySmooth.kerCotangentToTensor_injective_iff, derivationTensorProduct_algebraMap, tensorProductTo_surjective, Algebra.Extension.h1Cotangentι_apply, Algebra.Extension.cotangentComplex_injective_iff, mvPolynomialBasis_repr_D, ker_map_of_surjective, tensorKaehlerEquivOfFormallyEtale_symm_D_algebraMap, mvPolynomialBasis_repr_comp_D, Algebra.Generators.CotangentSpace.map_toComp_injective, Algebra.IsStandardSmooth.free_kaehlerDifferential, Algebra.Extension.Hom.sub_tmul, Algebra.SubmersivePresentation.rank_kaehlerDifferential, Algebra.SubmersivePresentation.sectionCotangent_comp, Algebra.formallySmooth_iff, isBaseChange_of_formallyEtale, Algebra.H1Cotangent.exact_map_δ, Algebra.Generators.H1Cotangent.δ_comp_equiv, mvPolynomialBasis_repr_symm_single, Algebra.IsStandardSmooth.iff_exists_basis_kaehlerDifferential, Algebra.SubmersivePresentation.sectionCotangent_zero_of_notMem_range, range_kerCotangentToTensor, map_D, Derivation.liftKaehlerDifferential_apply, Algebra.Generators.instFreeCotangentSpaceToExtension, instIsScalarTowerTensorProduct_1, DLinearMap_apply, Algebra.FormallySmooth.iff_injective_cotangentComplexBaseChange, Algebra.Generators.CotangentSpace.fst_compEquiv_apply, tensorKaehlerEquiv_tmul_D, Algebra.IsStandardSmoothOfRelativeDimension.rank_kaehlerDifferential, Algebra.smoothLocus_eq_compl_support_inter, Algebra.SubmersivePresentation.cotangentComplex_injective, mulActionBaseChange_smul_zero, Algebra.Extension.CotangentSpace.map_comp, Algebra.Extension.exact_cotangentComplex_toKaehler, Algebra.Generators.CotangentSpace.map_ofComp_surjective, map_liftBaseChange_smul, Algebra.Generators.H1Cotangent.map_comp_cotangentComplex_baseChange, quotKerTotalEquiv_apply, Algebra.Generators.CotangentSpace.fst_compEquiv, Algebra.Extension.CotangentSpace.map_comp_apply, Algebra.Generators.H1Cotangent.equiv_apply, Algebra.Extension.CotangentSpace.map_comp_cotangentComplex, instFreeMvPolynomialKaehlerDifferential, Algebra.H1Cotangent.exact_δ_mapBaseChange, instIsScalarTowerTensorProduct_2, Algebra.Generators.H1Cotangent.δ_map, Algebra.Extension.Cotangent.map_sub_map, mulActionBaseChange_smul_tmul, Algebra.FormallySmooth.iff_split_injection, Algebra.etaleLocus_eq_compl_support, Algebra.instFinitePresentationKaehlerDifferentialOfFinitePresentation, Algebra.Extension.cotangentComplex_mk, retractionOfSectionOfKerSqZero_tmul_D, linearCombination_surjective, derivationQuotKerSq_mk
quotKerTotalEquiv 📖	CompOp	3 math math: quotKerTotalEquiv_symm_comp_D, quotKerTotalEquiv_symm_apply, quotKerTotalEquiv_apply
quotientCotangentIdeal 📖	CompOp	—
quotientCotangentIdealRingEquiv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
DLinearMap_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring KaehlerDifferential NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential Algebra.toModule module' smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearMap.instFunLike DLinearMap TensorProduct Algebra.TensorProduct.instCommRing Ideal SetLike.instMembership Submodule.setLike NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule ideal Ideal.Cotangent Submodule.addCommMonoid Ideal.instAddCommGroupCotangent Submodule.module Ideal.instModuleCotangentOfAlgebra Algebra.id Ideal.toCotangent SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Algebra.TensorProduct.instRing TensorProduct.tmul AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne one_smul_sub_smul_one_mem_ideal	—	smulCommClass_self
D_apply 📖	mathematical	—	DFunLike.coe Derivation KaehlerDifferential CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential module' Algebra.id Algebra.to_smulCommClass CommSemiring.toSemiring smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toModule Derivation.instFunLike D LinearMap TensorProduct Algebra.TensorProduct.instCommRing RingHom.id Semiring.toNonAssocSemiring Ideal SetLike.instMembership Submodule.setLike NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule ideal Ideal.Cotangent Submodule.addCommMonoid Ideal.instAddCommGroupCotangent Submodule.module Ideal.instModuleCotangentOfAlgebra LinearMap.instFunLike Ideal.toCotangent SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Algebra.TensorProduct.instRing TensorProduct.tmul AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne one_smul_sub_smul_one_mem_ideal	—	Algebra.to_smulCommClass smulCommClass_self
D_tensorProductTo 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule KaehlerDifferential TensorProduct.addCommMonoid AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass module' Algebra.id LinearMap.instFunLike Derivation.tensorProductTo smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing isScalarTower_of_tower Algebra.toSMul IsScalarTower.right D Ideal Algebra.TensorProduct.instSemiring SetLike.instMembership Submodule.setLike NonAssocSemiring.toNonUnitalNonAssocSemiring ideal Algebra.TensorProduct.instCommRing Ideal.Cotangent Submodule.addCommMonoid Ideal.instAddCommGroupCotangent Submodule.module Ideal.instModuleCotangentOfAlgebra Ideal.toCotangent	—	Algebra.to_smulCommClass smulCommClass_self isScalarTower_of_tower IsScalarTower.right Derivation.liftKaehlerDifferential_apply Derivation.liftKaehlerDifferential_D
End_equiv_aux 📖	mathematical	—	AlgHom.comp HasQuotient.Quotient TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule CommSemiring.toSemiring Ideal Algebra.TensorProduct.instCommRing Ideal.instHasQuotient_1 Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring Submodule.idemSemiring Algebra.id ideal Ring.toSemiring Ideal.Quotient.instRingQuotient Ideal.instHasQuotient Ideal.cotangentIdeal Ideal.Quotient.ring Ideal.instIsTwoSided_1 Ideal.Quotient.commRing Ideal.instAlgebraQuotient Algebra.TensorProduct.instAlgebra Ideal.Quotient.algebra Ideal.Quotient.mkₐ IsScalarTower.toAlgHom Algebra.TensorProduct.leftAlgebra Algebra.to_smulCommClass Ideal.Quotient.isScalarTower Algebra.toSMul Algebra.TensorProduct.instRing CommRing.toRing TensorProduct.isScalarTower_left Module.toDistribMulAction NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring IsScalarTower.right RingHom.ker RingHom RingHom.instFunLike RingHom.instRingHomClass AlgHom.toRingHom Algebra.TensorProduct.lmul' Ideal.Quotient.semiring AlgHom.kerSquareLift AlgHom.id	—	Ideal.instIsTwoSided_1 Algebra.to_smulCommClass Ideal.Quotient.isScalarTower TensorProduct.isScalarTower_left IsScalarTower.right RingHom.instRingHomClass AlgHom.ext_iff Ideal.Quotient.mk_surjective mul_one RingEquiv.congr_arg RingEquiv.injective
derivationQuotKerTotal_apply 📖	mathematical	—	DFunLike.coe Derivation HasQuotient.Quotient Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Submodule CommSemiring.toSemiring CommRing.toCommSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule Submodule.hasQuotient CommRing.toRing Finsupp.instAddCommGroup Ring.toAddCommGroup kerTotal AddCommGroup.toAddCommMonoid Submodule.Quotient.addCommGroup Submodule.Quotient.module Submodule.Quotient.module' Algebra.toSMul Algebra.toModule Finsupp.isScalarTower DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toDistribSMul IsScalarTower.right Derivation.instFunLike derivationQuotKerTotal LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Submodule.mkQ Finsupp.single AddMonoidWithOne.toOne	—	Finsupp.isScalarTower IsScalarTower.right
derivationQuotKerTotal_lift_comp_linearCombination 📖	mathematical	—	LinearMap.comp Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring KaehlerDifferential HasQuotient.Quotient NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Submodule Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule Submodule.hasQuotient CommRing.toRing Finsupp.instAddCommGroup Ring.toAddCommGroup kerTotal AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential Submodule.Quotient.addCommGroup module' Algebra.id Algebra.to_smulCommClass Submodule.Quotient.module RingHom.id RingHomCompTriple.ids Derivation.liftKaehlerDifferential Submodule.Quotient.module' Algebra.toSMul Algebra.toModule Finsupp.isScalarTower DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toDistribSMul IsScalarTower.right Submodule.Quotient.isScalarTower SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero instDistribSMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Ring.toSemiring derivationQuotKerTotal Finsupp.linearCombination DFunLike.coe Derivation smulCommClass_self CommRing.toCommMonoid CommMonoid.toMonoid AddCommMonoid.toAddMonoid Derivation.instFunLike D Submodule.mkQ	—	Finsupp.lhom_ext Algebra.to_smulCommClass RingHomCompTriple.ids Finsupp.isScalarTower IsScalarTower.right Submodule.Quotient.isScalarTower smulCommClass_self Finsupp.smul_single_one map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass Finsupp.linearCombination_single Derivation.liftKaehlerDifferential_comp_D
exact_kerCotangentToTensor_mapBaseChange 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	Function.Exact Ideal.Cotangent RingHom.ker RingHom.instRingHomClass TensorProduct KaehlerDifferential NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential Algebra.toModule module' Algebra.id Algebra.to_smulCommClass LinearMap RingHom.id Ideal.instAddCommGroupCotangent TensorProduct.addCommMonoid Ideal.instModuleCotangentOfAlgebra TensorProduct.instModule LinearMap.instFunLike kerCotangentToTensor TensorProduct.leftModule Semiring.toModule mapBaseChange NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	Algebra.to_smulCommClass TensorProduct.isScalarTower_left IsScalarTower.right RingHom.instRingHomClass RingHomSurjective.ids SetLike.ext_iff range_kerCotangentToTensor
exact_mapBaseChange_map 📖	mathematical	—	Function.Exact TensorProduct CommRing.toCommSemiring KaehlerDifferential NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential Algebra.toModule CommSemiring.toSemiring module' Algebra.id Algebra.to_smulCommClass DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule LinearMap.instFunLike mapBaseChange map IsScalarTower.right NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	Algebra.to_smulCommClass IsScalarTower.right RingHomSurjective.ids SetLike.ext_iff range_mapBaseChange
finite 📖	mathematical	—	Module.Finite KaehlerDifferential CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential module' Algebra.id Algebra.to_smulCommClass	—	Algebra.to_smulCommClass smulCommClass_self top_le_iff span_range_derivation Submodule.span_le Algebra.adjoin_induction Submodule.subset_span Finset.mem_image_of_mem Derivation.map_algebraMap AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass AddMemClass.add_mem AddSubmonoidClass.toAddMemClass Derivation.map_add Derivation.leibniz Submodule.smul_mem MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Algebra.essFiniteType_cond_iff Algebra.EssFiniteType.cond add_sub_cancel_left smul_smul IsUnit.val_inv_mul one_smul sub_mem Submodule.addSubgroupClass
ideal_fg 📖	mathematical	—	Ideal.FG TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule CommSemiring.toSemiring Algebra.TensorProduct.instSemiring ideal	—	le_antisymm Finset.coe_image Ideal.span_le one_smul_sub_smul_one_mem_ideal span_range_eq_ideal Ideal.Quotient.isScalarTower IsScalarTower.right Algebra.EssFiniteType.algHom_ext Ideal.instIsTwoSided_1 Ideal.subset_span AlgHom.congr_fun
isScalarTower' 📖	mathematical	—	IsScalarTower TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule CommSemiring.toSemiring KaehlerDifferential TensorProduct.instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroupKaehlerDifferential DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Algebra.TensorProduct.instSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid instModuleTensorProductKaehlerDifferential module' smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing	—	Submodule.Quotient.isScalarTower smulCommClass_self IsScalarTower.right Submodule.isScalarTower'
isScalarTower_of_tower 📖	mathematical	—	IsScalarTower KaehlerDifferential SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroupKaehlerDifferential DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid module'	—	Submodule.Quotient.isScalarTower Submodule.isScalarTower' IsScalarTower.right TensorProduct.isScalarTower_left
kerCotangentToTensor_toCotangent 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Ideal.Cotangent RingHom.ker RingHom RingHom.instFunLike RingHom.instRingHomClass algebraMap TensorProduct KaehlerDifferential NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential Algebra.toModule module' Algebra.id Algebra.to_smulCommClass Ideal.instAddCommGroupCotangent TensorProduct.addCommMonoid Ideal.instModuleCotangentOfAlgebra TensorProduct.instModule LinearMap.instFunLike kerCotangentToTensor Ideal SetLike.instMembership Submodule.setLike NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Submodule.addCommMonoid Submodule.module Ideal.toCotangent TensorProduct.tmul AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Derivation smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring Derivation.instFunLike D	—	RingHom.instRingHomClass Algebra.to_smulCommClass
kerToTensor_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring 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 module' Algebra.id Algebra.to_smulCommClass Submodule.addCommMonoid TensorProduct.addCommMonoid Submodule.module TensorProduct.instModule LinearMap.instFunLike kerToTensor TensorProduct.tmul AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Derivation Derivation.instFunLike D	—	RingHom.instRingHomClass Algebra.to_smulCommClass
kerTotal_eq 📖	mathematical	—	LinearMap.ker Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring KaehlerDifferential Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential Finsupp.module Semiring.toModule module' Algebra.id Algebra.to_smulCommClass RingHom.id Finsupp.linearCombination DFunLike.coe Derivation smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toModule Derivation.instFunLike D kerTotal	—	le_antisymm Algebra.to_smulCommClass smulCommClass_self Submodule.ker_mkQ RingHomCompTriple.ids Finsupp.isScalarTower IsScalarTower.right Submodule.Quotient.isScalarTower derivationQuotKerTotal_lift_comp_linearCombination LinearMap.ker_le_ker_comp kerTotal.eq_1 Submodule.span_le map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass map_add SemilinearMapClass.toAddHomClass Finsupp.linearCombination_single one_smul AddMonoidHomClass.toAddHomClass Derivation.instAddMonoidHomClass smul_add sub_self Derivation.leibniz Derivation.map_algebraMap smul_zero
kerTotal_map 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	Submodule Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommMonoid Finsupp.module Algebra.toModule SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Submodule.map NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule RingHom.id RingHomSurjective.ids LinearMap.comp RingHomCompTriple.ids Finsupp.mapRange.linearMap Algebra.linearMap Finsupp.lmapDomain kerTotal Submodule.span Set.range Finsupp.single AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Submodule.restrictScalars MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Algebra.toSMul Finsupp.isScalarTower DistribSMul.toSMulZeroClass AddMonoidWithOne.toAddMonoid DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toDistribSMul IsScalarTower.right	—	RingHomSurjective.ids RingHomCompTriple.ids Finsupp.isScalarTower IsScalarTower.right kerTotal.eq_1 Submodule.map_span Submodule.restrictScalars_span Set.image_union Submodule.span_union Set.image_image Set.image_univ map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass map_add SemilinearMapClass.toAddHomClass Finsupp.mapDomain_single LinearMap.map_zero Finsupp.mapRange_single map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass sup_assoc Function.Surjective.range_comp Function.Surjective.prodMap sup_eq_right Submodule.span_mono IsScalarTower.algebraMap_apply Set.range_comp_subset_range
kerTotal_map' 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	Submodule.map Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommMonoid Finsupp.module Semiring.toModule Algebra.toModule RingHom.id RingHomSurjective.ids LinearMap.comp RingHomCompTriple.ids Finsupp.mapRange.linearMap Algebra.linearMap Finsupp.lmapDomain Submodule MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice kerTotal Submodule.span Set.range Finsupp.single AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Submodule.restrictScalars Algebra.toSMul Finsupp.isScalarTower DistribSMul.toSMulZeroClass AddMonoidWithOne.toAddMonoid DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toDistribSMul IsScalarTower.right	—	RingHomSurjective.ids RingHomCompTriple.ids Finsupp.isScalarTower IsScalarTower.right Submodule.map_sup kerTotal_map IsScalarTower.left Submodule.map_span Set.range_comp Finsupp.ext Finsupp.mapDomain_single LinearMap.map_zero Finsupp.mapRange_single map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsScalarTower.algebraMap_eq
kerTotal_mkQ_single_add 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid Finsupp.instAddCommGroup Ring.toAddCommGroup Finsupp.module CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule Submodule.hasQuotient kerTotal Submodule.Quotient.addCommGroup Submodule.Quotient.module LinearMap.instFunLike Submodule.mkQ Finsupp.single Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass sub_eq_zero map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass Submodule.mkQ_apply Submodule.Quotient.mk_eq_zero Finsupp.smul_single_one Submodule.smul_mem Submodule.subset_span
kerTotal_mkQ_single_algebraMap 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid Finsupp.instAddCommGroup Ring.toAddCommGroup Finsupp.module CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule Submodule.hasQuotient kerTotal Submodule.Quotient.addCommGroup Submodule.Quotient.module LinearMap.instFunLike Submodule.mkQ Finsupp.single RingHom RingHom.instFunLike algebraMap Submodule.Quotient.instZeroQuotient	—	Submodule.mkQ_apply Submodule.Quotient.mk_eq_zero Finsupp.smul_single_one Submodule.smul_mem Submodule.subset_span
kerTotal_mkQ_single_algebraMap_one 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid Finsupp.instAddCommGroup Ring.toAddCommGroup Finsupp.module CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule Submodule.hasQuotient kerTotal Submodule.Quotient.addCommGroup Submodule.Quotient.module LinearMap.instFunLike Submodule.mkQ Finsupp.single AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Submodule.Quotient.instZeroQuotient	—	RingHom.map_one kerTotal_mkQ_single_algebraMap
kerTotal_mkQ_single_mul 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid Finsupp.instAddCommGroup Ring.toAddCommGroup Finsupp.module CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule Submodule.hasQuotient kerTotal Submodule.Quotient.addCommGroup Submodule.Quotient.module LinearMap.instFunLike Submodule.mkQ Finsupp.single Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass sub_eq_zero map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass Submodule.mkQ_apply Submodule.Quotient.mk_eq_zero Finsupp.smul_single_one Submodule.smul_mem Submodule.subset_span
kerTotal_mkQ_single_smul 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid Finsupp.instAddCommGroup Ring.toAddCommGroup Finsupp.module CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule Submodule.hasQuotient kerTotal Submodule.Quotient.addCommGroup Submodule.Quotient.module LinearMap.instFunLike Submodule.mkQ Finsupp.single Algebra.toSMul Submodule.Quotient.instSMul' SMulZeroClass.toSMul Finsupp.instZero Finsupp.smulZeroClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.toModule Finsupp.isScalarTower NonUnitalNonAssocSemiring.toDistribSMul IsScalarTower.right	—	Finsupp.isScalarTower IsScalarTower.right Algebra.smul_def kerTotal_mkQ_single_mul kerTotal_mkQ_single_algebraMap add_zero LinearMap.map_smul_of_tower LinearMap.CompatibleSMul.finsupp_dom LinearMap.IsScalarTower.compatibleSMul' Submodule.Quotient.isScalarTower Finsupp.smul_single mul_comm
ker_map 📖	mathematical	—	LinearMap.ker KaehlerDifferential CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential module' Algebra.id Algebra.to_smulCommClass RingHom.id Semiring.toNonAssocSemiring map Submodule.map Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule RingHomSurjective.ids Finsupp.linearCombination DFunLike.coe Derivation smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toModule Derivation.instFunLike D Submodule.comap AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass LinearMap.comp RingHomCompTriple.ids Finsupp.mapRange.linearMap Algebra.linearMap Finsupp.lmapDomain RingHom RingHom.instFunLike algebraMap Submodule.restrictScalars Algebra.toSMul Finsupp.isScalarTower DistribSMul.toSMulZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalNonAssocSemiring.toDistribSMul IsScalarTower.right kerTotal	—	Algebra.to_smulCommClass RingHomSurjective.ids smulCommClass_self RingHomCompTriple.ids Finsupp.isScalarTower IsScalarTower.right Submodule.map_comap_eq_of_surjective linearCombination_surjective Submodule.ext Finsupp.apply_linearCombination Submodule.restrictScalars.congr_simp LinearMap.map_zero Finsupp.sum_mapRange_index zero_smul Finsupp.sum_mapDomain_index map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass add_smul algebraMap_smul isScalarTower_of_tower map_D
ker_map_of_surjective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	LinearMap.ker KaehlerDifferential AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential module' Algebra.id Algebra.to_smulCommClass IsScalarTower.to_smulCommClass NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule RingHom.id map IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Submodule.map Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Finsupp.instAddCommMonoid Finsupp.module Semiring.toModule RingHomSurjective.ids Finsupp.linearCombination Derivation smulCommClass_self CommRing.toCommMonoid CommMonoid.toMonoid Ring.toSemiring CommRing.toRing Derivation.instFunLike D AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass LinearMap.comp RingHomCompTriple.ids Finsupp.mapRange.linearMap Algebra.linearMap Finsupp.lmapDomain	—	Algebra.to_smulCommClass IsScalarTower.to_smulCommClass IsScalarTower.left RingHomSurjective.ids smulCommClass_self RingHomCompTriple.ids Finsupp.isScalarTower IsScalarTower.right ker_map kerTotal_map' Submodule.comap_map_eq Submodule.map_sup kerTotal_eq Submodule.comap_bot Submodule.map_comap_eq_of_surjective linearCombination_surjective bot_sup_eq Submodule.map_span Set.range_comp Submodule.span_eq_bot Finsupp.linearCombination_single Derivation.map_algebraMap smul_zero Zero.instNonempty
linearCombination_surjective 📖	mathematical	—	Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring KaehlerDifferential DFunLike.coe LinearMap RingHom.id Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential Finsupp.module Semiring.toModule module' Algebra.id Algebra.to_smulCommClass LinearMap.instFunLike Finsupp.linearCombination Derivation smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toModule Derivation.instFunLike D	—	Algebra.to_smulCommClass smulCommClass_self RingHomSurjective.ids LinearMap.range_eq_top Finsupp.range_linearCombination span_range_derivation
linearMapEquivDerivation_apply_apply 📖	mathematical	—	DFunLike.coe Derivation CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Derivation.instFunLike LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap KaehlerDifferential instAddCommGroupKaehlerDifferential module' Algebra.id Algebra.to_smulCommClass LinearMap.addCommMonoid Derivation.instAddCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Derivation.instModule IsScalarTower.to_smulCommClass EquivLike.toFunLike LinearEquiv.instEquivLike linearMapEquivDerivation LinearMap.instFunLike D	—	RingHomInvPair.ids Algebra.to_smulCommClass smulCommClass_self IsScalarTower.to_smulCommClass
linearMapEquivDerivation_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Derivation AddCommGroup.toAddCommMonoid LinearMap KaehlerDifferential instAddCommGroupKaehlerDifferential module' Algebra.id Algebra.to_smulCommClass Derivation.instAddCommMonoid LinearMap.addCommMonoid Derivation.instModule IsScalarTower.to_smulCommClass smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearMap.module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm linearMapEquivDerivation Derivation.liftKaehlerDifferential	—	Algebra.to_smulCommClass RingHomInvPair.ids IsScalarTower.to_smulCommClass smulCommClass_self
mapBaseChange_surjective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	TensorProduct KaehlerDifferential NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential Algebra.toModule module' Algebra.id Algebra.to_smulCommClass LinearMap RingHom.id TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule LinearMap.instFunLike mapBaseChange	—	subsingleton_of_surjective Algebra.to_smulCommClass RingHomSurjective.ids LinearMap.range_eq_top IsScalarTower.right range_mapBaseChange top_le_iff
mapBaseChange_tmul 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring 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 LinearMap.instFunLike mapBaseChange 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 IsScalarTower.to_smulCommClass NonAssocSemiring.toNonUnitalNonAssocSemiring map IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid	—	Algebra.to_smulCommClass IsScalarTower.to_smulCommClass IsScalarTower.left mul_one smul_eq_mul TensorProduct.smul_tmul' map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass IsBaseChange.lift_eq
map_D 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring KaehlerDifferential AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential module' Algebra.id Algebra.to_smulCommClass LinearMap.instFunLike map Derivation smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toModule Derivation.instFunLike D RingHom RingHom.instFunLike algebraMap	—	Derivation.congr_fun IsScalarTower.to_smulCommClass' Algebra.to_smulCommClass smulCommClass_self IsScalarTower.to_smulCommClass isScalarTower_of_tower IsScalarTower.right LinearMap.IsScalarTower.compatibleSMul map_compDer
map_compDer 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Derivation KaehlerDifferential AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential module' Algebra.id Algebra.to_smulCommClass smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toModule IsScalarTower.to_smulCommClass' NonAssocSemiring.toNonUnitalNonAssocSemiring Derivation.instAddCommMonoid Derivation.instModule IsScalarTower.to_smulCommClass isScalarTower_of_tower Algebra.toSMul IsScalarTower.right CommSemiring.toCommMonoid LinearMap.instFunLike LinearMap.compDer map D Derivation.compAlgebraMap Derivation.restrictScalars LinearMap.IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	Derivation.liftKaehlerDifferential_comp IsScalarTower.to_smulCommClass' isScalarTower_of_tower
map_surjective 📖	mathematical	—	KaehlerDifferential DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential module' Algebra.id Algebra.to_smulCommClass LinearMap.instFunLike map IsScalarTower.right	—	map_surjective_of_surjective IsScalarTower.right Algebra.to_smulCommClass
map_surjective_of_surjective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	KaehlerDifferential LinearMap RingHom.id AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential module' Algebra.id Algebra.to_smulCommClass LinearMap.instFunLike map	—	Algebra.to_smulCommClass RingHomSurjective.ids LinearMap.range_eq_top eq_top_iff isScalarTower_of_tower IsScalarTower.right Submodule.restrictScalars_top smulCommClass_self span_range_derivation Submodule.restrictScalars_span Submodule.span_le map_D
one_smul_sub_smul_one_mem_ideal 📖	mathematical	—	TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule CommSemiring.toSemiring Ideal Algebra.TensorProduct.instSemiring SetLike.instMembership Submodule.setLike NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule ideal SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Algebra.TensorProduct.instRing CommRing.toRing TensorProduct.tmul AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass one_mul mul_one sub_self
quotKerTotalEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids HasQuotient.Quotient Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Submodule Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule Submodule.hasQuotient CommRing.toRing Finsupp.instAddCommGroup Ring.toAddCommGroup kerTotal KaehlerDifferential AddCommGroup.toAddCommMonoid Submodule.Quotient.addCommGroup instAddCommGroupKaehlerDifferential Submodule.Quotient.module module' Algebra.id Algebra.to_smulCommClass EquivLike.toFunLike LinearEquiv.instEquivLike quotKerTotalEquiv AddMonoidHom AddSubgroup AddCommGroup.toAddGroup QuotientAddGroup.instHasQuotientAddSubgroup Submodule.toAddSubgroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid QuotientAddGroup.Quotient.addGroup AddCommMonoid.toAddMonoid AddMonoidHom.instFunLike QuotientAddGroup.lift LinearMap.toAddMonoidHom Ring.toSemiring Finsupp.linearCombination Derivation Derivation.instFunLike D	—	RingHomInvPair.ids Algebra.to_smulCommClass
quotKerTotalEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids KaehlerDifferential HasQuotient.Quotient Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Submodule Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule Submodule.hasQuotient CommRing.toRing Finsupp.instAddCommGroup Ring.toAddCommGroup kerTotal AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential Submodule.Quotient.addCommGroup module' Algebra.id Algebra.to_smulCommClass Submodule.Quotient.module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm quotKerTotalEquiv LinearMap LinearMap.instFunLike Derivation.liftKaehlerDifferential Submodule.Quotient.module' Algebra.toSMul Algebra.toModule derivationQuotKerTotal	—	RingHomInvPair.ids Algebra.to_smulCommClass
quotKerTotalEquiv_symm_comp_D 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Derivation KaehlerDifferential AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential module' Algebra.id Algebra.to_smulCommClass smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toModule HasQuotient.Quotient Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Submodule Finsupp.instAddCommMonoid Finsupp.module Semiring.toModule Submodule.hasQuotient Finsupp.instAddCommGroup Ring.toAddCommGroup kerTotal Submodule.Quotient.addCommGroup Submodule.Quotient.module Submodule.Quotient.module' Algebra.toSMul Finsupp.isScalarTower DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero NonUnitalNonAssocSemiring.toDistribSMul IsScalarTower.right Derivation.instAddCommMonoid Derivation.instModule IsScalarTower.to_smulCommClass isScalarTower_of_tower CommSemiring.toCommMonoid Submodule.Quotient.isScalarTower SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero instDistribSMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing LinearMap.instFunLike LinearMap.compDer LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv.symm quotKerTotalEquiv D derivationQuotKerTotal	—	Finsupp.isScalarTower IsScalarTower.right Algebra.to_smulCommClass smulCommClass_self IsScalarTower.to_smulCommClass isScalarTower_of_tower Submodule.Quotient.isScalarTower RingHomInvPair.ids Derivation.liftKaehlerDifferential_comp
range_kerCotangentToTensor 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	LinearMap.range Ideal.Cotangent RingHom.ker RingHom.instRingHomClass TensorProduct KaehlerDifferential NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential Algebra.toModule module' Algebra.id Algebra.to_smulCommClass Ideal.instAddCommGroupCotangent TensorProduct.addCommMonoid Ideal.instModuleCotangentOfAlgebra TensorProduct.instModule RingHom.id RingHomSurjective.ids kerCotangentToTensor Submodule.restrictScalars TensorProduct.leftModule Semiring.toModule Algebra.toSMul TensorProduct.isScalarTower_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsScalarTower.right LinearMap.ker mapBaseChange	—	Submodule.ext Algebra.to_smulCommClass RingHom.instRingHomClass RingHomSurjective.ids TensorProduct.isScalarTower_left IsScalarTower.right Ideal.toCotangent_surjective smulCommClass_self IsScalarTower.to_smulCommClass IsScalarTower.left mapBaseChange_tmul map_D RingHom.mem_ker map_zero AddMonoidHomClass.toZeroHomClass Derivation.instAddMonoidHomClass smul_zero LinearMap.rTensor_surjective RingHomInvPair.ids LinearEquiv.surjective map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass one_smul RingHomCompTriple.ids ker_map_of_surjective Finsupp.sum_single Finsupp.sum.eq_1 Finset.sum_fiberwise_of_maps_to Finset.mem_image_of_mem map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass TensorProduct.tmul_sum sum_mem Submodule.addSubmonoidClass Finset.sum_congr Finsupp.linearCombination_single RingHomClass.toAddMonoidHomClass Finsupp.mapRange_single LinearMap.map_zero Finsupp.finset_sum_apply Finsupp.single_apply DFunLike.congr_fun Subtype.prop map_sub sub_self LinearMapClass.map_smul TensorProduct.CompatibleSMul.isScalarTower isScalarTower_of_tower smul_sub TensorProduct.tmul_sub Finset.sum_sub_distrib Finset.sum_attach TensorProduct.smul_tmul Algebra.algebraMap_eq_smul_one TensorProduct.zero_tmul
range_mapBaseChange 📖	mathematical	—	LinearMap.range TensorProduct CommRing.toCommSemiring KaehlerDifferential NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential Algebra.toModule CommSemiring.toSemiring module' Algebra.id Algebra.to_smulCommClass TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids mapBaseChange LinearMap.ker map IsScalarTower.right	—	le_antisymm Algebra.to_smulCommClass RingHomSurjective.ids IsScalarTower.right TensorProduct.induction_on map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass smulCommClass_self linearCombination_surjective IsScalarTower.to_smulCommClass IsScalarTower.left mapBaseChange_tmul map_smul SemilinearMapClass.toMulActionSemiHomClass Finsupp.induction_linear smul_zero map_add SemilinearMapClass.toAddHomClass smul_add add_zero Finsupp.linearCombination_single map_D LinearMap.map_smul_of_tower LinearMap.IsScalarTower.compatibleSMul isScalarTower_of_tower RingHomCompTriple.comp_apply RingHomCompTriple.right_ids Derivation.map_algebraMap AddMemClass.add_mem AddSubmonoidClass.toAddMemClass RingHomCompTriple.ids Finsupp.isScalarTower ker_map Finsupp.lhom_ext' LinearMap.ext_ring Finsupp.ext LinearMap.comp.congr_simp Finsupp.mapRange.linearMap_id Finsupp.lmapDomain_id Submodule.comap_id Submodule.map_le_iff_le_comap kerTotal.eq_1 Submodule.span_le map_sub one_smul AddMonoidHomClass.toAddHomClass Derivation.instAddMonoidHomClass sub_self Derivation.leibniz
span_range_derivation 📖	mathematical	—	Submodule.span KaehlerDifferential CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential module' Algebra.id Algebra.to_smulCommClass Set.range DFunLike.coe Derivation smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toModule Derivation.instFunLike D Top.top Submodule Submodule.instTop	—	Algebra.to_smulCommClass smulCommClass_self eq_top_iff Ideal.toCotangent_surjective IsScalarTower.right Submodule.span_induction one_smul_sub_smul_one_mem_ideal Submodule.subset_span DLinearMap_apply ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass Submodule.zero_mem AddMemClass.add_mem AddSubmonoidClass.toAddMemClass Submodule.add_mem Submodule.smul_mem submodule_span_range_eq_ideal
span_range_eq_ideal 📖	mathematical	—	Ideal.span TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule CommSemiring.toSemiring Algebra.TensorProduct.instSemiring Set.range SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Algebra.TensorProduct.instRing CommRing.toRing TensorProduct.tmul AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne ideal	—	le_antisymm Ideal.span_le one_smul_sub_smul_one_mem_ideal Algebra.to_smulCommClass IsScalarTower.right submodule_span_range_eq_ideal Ideal.span.eq_1 Submodule.span_span_of_tower Submodule.subset_span
submodule_span_range_eq_ideal 📖	mathematical	—	Submodule.span TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass Set.range SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Algebra.TensorProduct.instRing CommRing.toRing TensorProduct.tmul AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Submodule.restrictScalars Algebra.TensorProduct.instSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring TensorProduct.leftHasSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsScalarTower.right Algebra.TensorProduct.leftAlgebra Algebra.id ideal	—	le_antisymm Algebra.to_smulCommClass IsScalarTower.right Submodule.span_le one_smul_sub_smul_one_mem_ideal TensorProduct.zero_tmul sub_zero TensorProduct.induction_on map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass smul_sub mul_one Algebra.TensorProduct.lmul'_apply_tmul Submodule.smul_mem Submodule.subset_span Set.mem_range_self map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass TensorProduct.add_tmul sub_add_sub_comm AddMemClass.add_mem AddSubmonoidClass.toAddMemClass
subsingleton_of_surjective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	KaehlerDifferential	—	Algebra.to_smulCommClass smulCommClass_self span_range_derivation Submodule.span_le Derivation.map_algebraMap
tensorProductTo_surjective 📖	mathematical	—	TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule CommSemiring.toSemiring KaehlerDifferential DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring TensorProduct.addCommMonoid AddCommGroup.toAddCommMonoid instAddCommGroupKaehlerDifferential TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass module' Algebra.id LinearMap.instFunLike Derivation.tensorProductTo smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing isScalarTower_of_tower Algebra.toSMul IsScalarTower.right D	—	Algebra.to_smulCommClass smulCommClass_self isScalarTower_of_tower IsScalarTower.right Ideal.toCotangent_surjective D_tensorProductTo

(root)

Definitions

Name	Category	Theorems
KaehlerDifferential 📖	CompOp	168 math math: KaehlerDifferential.kerCotangentToTensor_toCotangent, KaehlerDifferential.mvPolynomialBasis_apply, Algebra.Presentation.differentials.comm₁₂_single, Algebra.Generators.H1Cotangent.δAux_mul, Algebra.Presentation.differentialsSolution_isPresentation, KaehlerDifferential.polynomialEquiv_symm, Algebra.Extension.H1Cotangent.equiv_apply, KaehlerDifferential.tensorKaehlerEquiv_symm_D_tmul', Algebra.Generators.cotangentSpaceBasis_apply, KaehlerDifferential.mvPolynomialBasis_repr_D_X, KaehlerDifferential.tensorKaehlerEquiv_symm_D_tmul, Algebra.FormallySmooth.projective_kaehlerDifferential, Algebra.Presentation.differentials.comm₂₃, KaehlerDifferential.cotangentComplexBaseChange_tmul, Algebra.Extension.formallySmooth_iff_split_injection, KaehlerDifferential.polynomialEquiv_D, Algebra.FormallySmooth.instFinitePresentationKaehlerDifferentialOfEssFiniteType, Algebra.Extension.CotangentSpace.map_id, KaehlerDifferential.kerToTensor_apply, KaehlerDifferential.isScalarTower', KaehlerDifferential.quotKerTotalEquiv_symm_comp_D, Algebra.formallyUnramified_iff, Algebra.Extension.lTensor_cotangentComplex_eq_cotangentComplexBaseChange, KaehlerDifferential.isLocalizedModule_of_isLocalizedModule, Algebra.IsStandardSmoothOfRelationDimension.subsingleton_kaehlerDifferential, Algebra.Generators.cotangentSpaceBasis_repr_one_tmul, KaehlerDifferential.instIsScalarTowerTensorProduct, Algebra.SubmersivePresentation.basisKaehlerOfIsCompl_apply, retractionOfSectionOfKerSqZero_comp_kerToTensor, KaehlerDifferential.mapBaseChange_tmul, KaehlerDifferential.kerTotal_eq, Algebra.Generators.H1Cotangent.δAux_C, Algebra.FormallySmooth.iff_injective_cotangentComplexBaseChange_residueField, Algebra.Extension.subsingleton_h1Cotangent, Algebra.Extension.CotangentSpace.map_tmul, KaehlerDifferential.polynomialEquiv_comp_D, KaehlerDifferential.span_range_map_derivation_of_isLocalization, Algebra.Extension.H1Cotangent.val_zero, KaehlerDifferential.mulActionBaseChange_smul_add, Algebra.FormallySmooth.iff_injective_lTensor_residueField, Algebra.formallyEtale_iff, Algebra.IsStandardSmoothOfRelativeDimension.iff_of_isStandardSmooth, KaehlerDifferential.linearMapEquivDerivation_apply_apply, KaehlerDifferential.tensorKaehlerEquivBase_tmul, Algebra.FormallySmooth.iff_subsingleton_and_projective, KaehlerDifferential.tensorKaehlerEquivBase_symm_apply, KaehlerDifferential.isLocalizedModule_map, KaehlerDifferential.isScalarTower_of_tower, KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale_apply, KaehlerDifferential.linearMapEquivDerivation_symm_apply, KaehlerDifferential.span_range_derivation, Algebra.Generators.H1Cotangent.exact_map_δ, Algebra.Generators.H1Cotangent.δAux_monomial, Algebra.Generators.CotangentSpace.compEquiv_symm_zero, Algebra.Generators.cotangentSpaceBasis_repr_tmul, Algebra.Extension.Hom.sub_one_tmul, KaehlerDifferential.exact_mapBaseChange_map, KaehlerDifferential.tensorKaehlerEquiv_tmul, Algebra.Generators.H1Cotangent.δAux_toAlgHom, KaehlerDifferential.D_apply, Algebra.Extension.CotangentSpace.map_toInfinitesimal_bijective, KaehlerDifferential.range_mapBaseChange, Algebra.SubmersivePresentation.sectionCotangent_eq_iff, Algebra.Generators.H1Cotangent.exact_δ_map, Derivation.liftKaehlerDifferential_comp, KaehlerDifferential.ker_map, KaehlerDifferential.mapBaseChange_surjective, KaehlerDifferential.subsingleton_of_surjective, Algebra.Extension.CotangentSpace.map_sub_map, KaehlerDifferential.map_surjective_of_surjective, Algebra.unramifiedLocus_eq_compl_support, KaehlerDifferential.finite, Algebra.Extension.CotangentSpace.map_cotangentComplex, Algebra.Extension.cotangentComplexBaseChange_eq_lTensor_cotangentComplex, tensorKaehlerQuotKerSqEquiv_symm_tmul_D, Derivation.liftKaehlerDifferential_comp_D, Algebra.Generators.H1Cotangent.δAux_ofComp, Algebra.Presentation.differentials.comm₂₃', KaehlerDifferential.instSMulCommClassTensorProduct_1, KaehlerDifferential.tensorKaehlerEquiv_left_inv, Derivation.liftKaehlerDifferential_unique_iff, Derivation.liftKaehlerDifferential_D, tensorKaehlerQuotKerSqEquiv_tmul_D, KaehlerDifferential.isBaseChange, KaehlerDifferential.instSMulCommClassTensorProduct, KaehlerDifferential.mvPolynomialBasis_repr_apply, Algebra.FormallyEtale.subsingleton_kaehlerDifferential, Algebra.Extension.h1Cotangentι_ext_iff, Algebra.Generators.toKaehler_tmul_D, KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange, Algebra.Extension.H1Cotangent.val_add, Algebra.Extension.H1Cotangent.val_smul, Algebra.Presentation.differentials.comm₁₂, KaehlerDifferential.map_surjective, KaehlerDifferential.map_compDer, Algebra.SubmersivePresentation.free_kaehlerDifferential, Algebra.Generators.H1Cotangent.exact_map_δ', KaehlerDifferential.D_tensorProductTo, Algebra.Extension.toKaehler_surjective, Algebra.Generators.CotangentSpace.exact, Algebra.Generators.H1Cotangent.δAux_X, KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination, Algebra.Generators.repr_CotangentSpaceMap, KaehlerDifferential.isLocalizedModule, Algebra.Extension.H1Cotangent.map_apply_coe, Algebra.Generators.toKaehler_cotangentSpaceBasis, Algebra.SubmersivePresentation.basisKaehler_apply, KaehlerDifferential.polynomial_D_apply, Algebra.Generators.CotangentSpace.compEquiv_symm_inr, KaehlerDifferential.quotKerTotalEquiv_symm_apply, Algebra.FormallySmooth.kerCotangentToTensor_injective_iff, KaehlerDifferential.derivationTensorProduct_algebraMap, KaehlerDifferential.tensorProductTo_surjective, Algebra.Extension.h1Cotangentι_apply, Algebra.Extension.cotangentComplex_injective_iff, KaehlerDifferential.mvPolynomialBasis_repr_D, KaehlerDifferential.ker_map_of_surjective, KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale_symm_D_algebraMap, KaehlerDifferential.mvPolynomialBasis_repr_comp_D, Algebra.Generators.CotangentSpace.map_toComp_injective, Algebra.IsStandardSmooth.free_kaehlerDifferential, Algebra.Extension.Hom.sub_tmul, Algebra.SubmersivePresentation.rank_kaehlerDifferential, Algebra.SubmersivePresentation.sectionCotangent_comp, Algebra.formallySmooth_iff, KaehlerDifferential.isBaseChange_of_formallyEtale, Algebra.H1Cotangent.exact_map_δ, Algebra.Generators.H1Cotangent.δ_comp_equiv, KaehlerDifferential.mvPolynomialBasis_repr_symm_single, Algebra.IsStandardSmooth.iff_exists_basis_kaehlerDifferential, Algebra.SubmersivePresentation.sectionCotangent_zero_of_notMem_range, KaehlerDifferential.range_kerCotangentToTensor, KaehlerDifferential.map_D, Derivation.liftKaehlerDifferential_apply, Algebra.Generators.instFreeCotangentSpaceToExtension, KaehlerDifferential.instIsScalarTowerTensorProduct_1, KaehlerDifferential.DLinearMap_apply, Algebra.FormallySmooth.iff_injective_cotangentComplexBaseChange, Algebra.Generators.CotangentSpace.fst_compEquiv_apply, KaehlerDifferential.tensorKaehlerEquiv_tmul_D, Algebra.IsStandardSmoothOfRelativeDimension.rank_kaehlerDifferential, Algebra.smoothLocus_eq_compl_support_inter, Algebra.SubmersivePresentation.cotangentComplex_injective, KaehlerDifferential.mulActionBaseChange_smul_zero, Algebra.Extension.CotangentSpace.map_comp, Algebra.Extension.exact_cotangentComplex_toKaehler, Algebra.Generators.CotangentSpace.map_ofComp_surjective, KaehlerDifferential.map_liftBaseChange_smul, Algebra.Generators.H1Cotangent.map_comp_cotangentComplex_baseChange, KaehlerDifferential.quotKerTotalEquiv_apply, Algebra.Generators.CotangentSpace.fst_compEquiv, Algebra.Extension.CotangentSpace.map_comp_apply, Algebra.Generators.H1Cotangent.equiv_apply, Algebra.Extension.CotangentSpace.map_comp_cotangentComplex, instFreeMvPolynomialKaehlerDifferential, Algebra.FormallyUnramified.subsingleton_kaehlerDifferential, Algebra.H1Cotangent.exact_δ_mapBaseChange, KaehlerDifferential.instIsScalarTowerTensorProduct_2, Algebra.Generators.H1Cotangent.δ_map, Algebra.Extension.Cotangent.map_sub_map, KaehlerDifferential.mulActionBaseChange_smul_tmul, Algebra.FormallySmooth.iff_split_injection, Algebra.etaleLocus_eq_compl_support, Algebra.instFinitePresentationKaehlerDifferentialOfFinitePresentation, Algebra.Extension.cotangentComplex_mk, retractionOfSectionOfKerSqZero_tmul_D, KaehlerDifferential.linearCombination_surjective, derivationQuotKerSq_mk
instAddCommGroupKaehlerDifferential 📖	CompOp	162 math math: KaehlerDifferential.kerCotangentToTensor_toCotangent, KaehlerDifferential.mvPolynomialBasis_apply, Algebra.Presentation.differentials.comm₁₂_single, Algebra.Generators.H1Cotangent.δAux_mul, Algebra.Presentation.differentialsSolution_isPresentation, KaehlerDifferential.polynomialEquiv_symm, Algebra.Extension.H1Cotangent.equiv_apply, KaehlerDifferential.tensorKaehlerEquiv_symm_D_tmul', Algebra.Generators.cotangentSpaceBasis_apply, KaehlerDifferential.mvPolynomialBasis_repr_D_X, KaehlerDifferential.tensorKaehlerEquiv_symm_D_tmul, Algebra.FormallySmooth.projective_kaehlerDifferential, Algebra.Presentation.differentials.comm₂₃, KaehlerDifferential.cotangentComplexBaseChange_tmul, Algebra.Extension.formallySmooth_iff_split_injection, KaehlerDifferential.polynomialEquiv_D, Algebra.FormallySmooth.instFinitePresentationKaehlerDifferentialOfEssFiniteType, Algebra.Extension.CotangentSpace.map_id, KaehlerDifferential.kerToTensor_apply, KaehlerDifferential.isScalarTower', KaehlerDifferential.quotKerTotalEquiv_symm_comp_D, Algebra.Extension.lTensor_cotangentComplex_eq_cotangentComplexBaseChange, KaehlerDifferential.isLocalizedModule_of_isLocalizedModule, Algebra.Generators.cotangentSpaceBasis_repr_one_tmul, KaehlerDifferential.instIsScalarTowerTensorProduct, Algebra.SubmersivePresentation.basisKaehlerOfIsCompl_apply, retractionOfSectionOfKerSqZero_comp_kerToTensor, KaehlerDifferential.mapBaseChange_tmul, KaehlerDifferential.kerTotal_eq, Algebra.Generators.H1Cotangent.δAux_C, Algebra.FormallySmooth.iff_injective_cotangentComplexBaseChange_residueField, Algebra.Extension.subsingleton_h1Cotangent, Algebra.Extension.CotangentSpace.map_tmul, KaehlerDifferential.polynomialEquiv_comp_D, KaehlerDifferential.span_range_map_derivation_of_isLocalization, Algebra.Extension.H1Cotangent.val_zero, KaehlerDifferential.mulActionBaseChange_smul_add, Algebra.FormallySmooth.iff_injective_lTensor_residueField, Algebra.IsStandardSmoothOfRelativeDimension.iff_of_isStandardSmooth, KaehlerDifferential.linearMapEquivDerivation_apply_apply, KaehlerDifferential.tensorKaehlerEquivBase_tmul, Algebra.FormallySmooth.iff_subsingleton_and_projective, KaehlerDifferential.tensorKaehlerEquivBase_symm_apply, KaehlerDifferential.isLocalizedModule_map, KaehlerDifferential.isScalarTower_of_tower, KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale_apply, KaehlerDifferential.linearMapEquivDerivation_symm_apply, KaehlerDifferential.span_range_derivation, Algebra.Generators.H1Cotangent.exact_map_δ, Algebra.Generators.H1Cotangent.δAux_monomial, Algebra.Generators.CotangentSpace.compEquiv_symm_zero, Algebra.Generators.cotangentSpaceBasis_repr_tmul, Algebra.Extension.Hom.sub_one_tmul, KaehlerDifferential.exact_mapBaseChange_map, KaehlerDifferential.tensorKaehlerEquiv_tmul, Algebra.Generators.H1Cotangent.δAux_toAlgHom, KaehlerDifferential.D_apply, Algebra.Extension.CotangentSpace.map_toInfinitesimal_bijective, KaehlerDifferential.range_mapBaseChange, Algebra.SubmersivePresentation.sectionCotangent_eq_iff, Algebra.Generators.H1Cotangent.exact_δ_map, Derivation.liftKaehlerDifferential_comp, KaehlerDifferential.ker_map, KaehlerDifferential.mapBaseChange_surjective, Algebra.Extension.CotangentSpace.map_sub_map, KaehlerDifferential.map_surjective_of_surjective, Algebra.unramifiedLocus_eq_compl_support, KaehlerDifferential.finite, Algebra.Extension.CotangentSpace.map_cotangentComplex, Algebra.Extension.cotangentComplexBaseChange_eq_lTensor_cotangentComplex, tensorKaehlerQuotKerSqEquiv_symm_tmul_D, Derivation.liftKaehlerDifferential_comp_D, Algebra.Generators.H1Cotangent.δAux_ofComp, Algebra.Presentation.differentials.comm₂₃', KaehlerDifferential.instSMulCommClassTensorProduct_1, KaehlerDifferential.tensorKaehlerEquiv_left_inv, Derivation.liftKaehlerDifferential_unique_iff, Derivation.liftKaehlerDifferential_D, tensorKaehlerQuotKerSqEquiv_tmul_D, KaehlerDifferential.isBaseChange, KaehlerDifferential.instSMulCommClassTensorProduct, KaehlerDifferential.mvPolynomialBasis_repr_apply, Algebra.Extension.h1Cotangentι_ext_iff, Algebra.Generators.toKaehler_tmul_D, KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange, Algebra.Extension.H1Cotangent.val_add, Algebra.Extension.H1Cotangent.val_smul, Algebra.Presentation.differentials.comm₁₂, KaehlerDifferential.map_surjective, KaehlerDifferential.map_compDer, Algebra.SubmersivePresentation.free_kaehlerDifferential, Algebra.Generators.H1Cotangent.exact_map_δ', KaehlerDifferential.D_tensorProductTo, Algebra.Extension.toKaehler_surjective, Algebra.Generators.CotangentSpace.exact, Algebra.Generators.H1Cotangent.δAux_X, KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination, Algebra.Generators.repr_CotangentSpaceMap, KaehlerDifferential.isLocalizedModule, Algebra.Extension.H1Cotangent.map_apply_coe, Algebra.Generators.toKaehler_cotangentSpaceBasis, Algebra.SubmersivePresentation.basisKaehler_apply, KaehlerDifferential.polynomial_D_apply, Algebra.Generators.CotangentSpace.compEquiv_symm_inr, KaehlerDifferential.quotKerTotalEquiv_symm_apply, Algebra.FormallySmooth.kerCotangentToTensor_injective_iff, KaehlerDifferential.derivationTensorProduct_algebraMap, KaehlerDifferential.tensorProductTo_surjective, Algebra.Extension.h1Cotangentι_apply, Algebra.Extension.cotangentComplex_injective_iff, KaehlerDifferential.mvPolynomialBasis_repr_D, KaehlerDifferential.ker_map_of_surjective, KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale_symm_D_algebraMap, KaehlerDifferential.mvPolynomialBasis_repr_comp_D, Algebra.Generators.CotangentSpace.map_toComp_injective, Algebra.IsStandardSmooth.free_kaehlerDifferential, Algebra.Extension.Hom.sub_tmul, Algebra.SubmersivePresentation.rank_kaehlerDifferential, Algebra.SubmersivePresentation.sectionCotangent_comp, Algebra.formallySmooth_iff, KaehlerDifferential.isBaseChange_of_formallyEtale, Algebra.H1Cotangent.exact_map_δ, Algebra.Generators.H1Cotangent.δ_comp_equiv, KaehlerDifferential.mvPolynomialBasis_repr_symm_single, Algebra.IsStandardSmooth.iff_exists_basis_kaehlerDifferential, Algebra.SubmersivePresentation.sectionCotangent_zero_of_notMem_range, KaehlerDifferential.range_kerCotangentToTensor, KaehlerDifferential.map_D, Derivation.liftKaehlerDifferential_apply, Algebra.Generators.instFreeCotangentSpaceToExtension, KaehlerDifferential.instIsScalarTowerTensorProduct_1, KaehlerDifferential.DLinearMap_apply, Algebra.FormallySmooth.iff_injective_cotangentComplexBaseChange, Algebra.Generators.CotangentSpace.fst_compEquiv_apply, KaehlerDifferential.tensorKaehlerEquiv_tmul_D, Algebra.IsStandardSmoothOfRelativeDimension.rank_kaehlerDifferential, Algebra.smoothLocus_eq_compl_support_inter, Algebra.SubmersivePresentation.cotangentComplex_injective, KaehlerDifferential.mulActionBaseChange_smul_zero, Algebra.Extension.CotangentSpace.map_comp, Algebra.Extension.exact_cotangentComplex_toKaehler, Algebra.Generators.CotangentSpace.map_ofComp_surjective, KaehlerDifferential.map_liftBaseChange_smul, Algebra.Generators.H1Cotangent.map_comp_cotangentComplex_baseChange, KaehlerDifferential.quotKerTotalEquiv_apply, Algebra.Generators.CotangentSpace.fst_compEquiv, Algebra.Extension.CotangentSpace.map_comp_apply, Algebra.Generators.H1Cotangent.equiv_apply, Algebra.Extension.CotangentSpace.map_comp_cotangentComplex, instFreeMvPolynomialKaehlerDifferential, Algebra.H1Cotangent.exact_δ_mapBaseChange, KaehlerDifferential.instIsScalarTowerTensorProduct_2, Algebra.Generators.H1Cotangent.δ_map, Algebra.Extension.Cotangent.map_sub_map, KaehlerDifferential.mulActionBaseChange_smul_tmul, Algebra.FormallySmooth.iff_split_injection, Algebra.etaleLocus_eq_compl_support, Algebra.instFinitePresentationKaehlerDifferentialOfFinitePresentation, Algebra.Extension.cotangentComplex_mk, retractionOfSectionOfKerSqZero_tmul_D, KaehlerDifferential.linearCombination_surjective, derivationQuotKerSq_mk
instInhabitedKaehlerDifferential 📖	CompOp	—
instIsScalarTowerTensorProductKaehlerDifferential 📖	CompOp	—
instModuleTensorProductKaehlerDifferential 📖	CompOp	1 math math: KaehlerDifferential.isScalarTower'
instR 📖	CompOp	—
«termΩ[_⁄_]» 📖	CompOp	—

---

← Back to Index