Basic

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

Statistics

Metric	Count
Definitions apply, coeFnAddMonoidHom, compAlgebraMap, compAlgebraMapL, hasCoeToLinearMap, instAdd, instAddCommGroup, instAddCommMonoid, instDistribMulAction, instFunLike, instInhabited, instModule, instNeg, instSMul, instSub, instZero, liftOfRightInverse, liftOfSurjective, llcomp, mk', restrictScalars, toLinearMap, compDer, compDer	24
Theorems add_apply, coeFnAddMonoidHom_apply, coeFn_coe, coe_add, coe_add_linearMap, coe_comp, coe_injective, coe_mk', coe_mk'_linearMap, coe_neg, coe_neg_linearMap, coe_restrictScalars, coe_smul, coe_smul_linearMap, coe_sub, coe_sub_linearMap, coe_to_linearMap_comp, coe_zero, coe_zero_linearMap, compAlgebraMapL_apply_apply, compAlgebraMap_apply, congr_fun, eqOn_adjoin, ext, ext_iff, ext_of_adjoin_eq_top, instAddMonoidHomClass, instIsCentralScalar, instIsScalarTower, instSMulCommClass, leibniz, leibniz', leibniz_div, leibniz_div_const, leibniz_inv, leibniz_invOf, leibniz_of_mul_eq_one, leibniz_pow, leibniz_zpow, liftOfRightInverse_apply, liftOfRightInverse_eq, liftOfSurjective_apply, linearEquiv_coe_comp, linearEquiv_coe_to_linearMap_comp, llcomp_apply, map_add, map_aeval, map_algebraMap, map_intCast, map_natCast, map_neg, map_one_eq_zero, map_one_eq_zero', map_smul, map_smul_of_tower, map_sub, map_zero, mk_coe, neg_apply, restrictScalars_apply, smul_apply, sub_apply, toFun_eq_coe, zero_apply	64
Total	88

Derivation

Definitions

Name	Category	Theorems
coeFnAddMonoidHom 📖	CompOp	1 math math: coeFnAddMonoidHom_apply
compAlgebraMap 📖	CompOp	3 math math: KaehlerDifferential.map_compDer, compAlgebraMap_apply, apply_aeval_eq
compAlgebraMapL 📖	CompOp	1 math math: compAlgebraMapL_apply_apply
hasCoeToLinearMap 📖	CompOp	—
instAdd 📖	CompOp	4 math math: coe_add, LeftInvariantDerivation.lift_add, add_apply, coe_add_linearMap
instAddCommGroup 📖	CompOp	—
instAddCommMonoid 📖	CompOp	31 math math: coe_to_linearMap_comp, LeftInvariantDerivation.left_invariant', LeftInvariantDerivation.left_invariant, linearEquiv_coe_to_linearMap_comp, KaehlerDifferential.quotKerTotalEquiv_symm_comp_D, KaehlerDifferential.polynomialEquiv_comp_D, Polynomial.mkDerivation_one_eq_derivative', KaehlerDifferential.linearMapEquivDerivation_apply_apply, LeftInvariantDerivation.evalAt_coe, KaehlerDifferential.linearMapEquivDerivation_symm_apply, fdifferential_apply, coeFnAddMonoidHom_apply, liftKaehlerDifferential_comp, LeftInvariantDerivation.left_invariant'', compAlgebraMapL_apply_apply, Polynomial.mkDerivationEquiv_symm_apply, coe_comp, Polynomial.mkDerivationEquiv_apply, liftKaehlerDifferential_unique_iff, llcomp_apply, fdifferential_comp, KaehlerDifferential.map_compDer, hfdifferential_apply, Polynomial.mkDerivation_X, Polynomial.mkDerivation_one_eq_derivative, KaehlerDifferential.mvPolynomialBasis_repr_comp_D, LeftInvariantDerivation.evalAt_mul, linearEquiv_coe_comp, Polynomial.mkDerivation_apply, evalAt_apply, LeftInvariantDerivation.evalAt_apply
instDistribMulAction 📖	CompOp	—
instFunLike 📖	CompOp	193 math math: map_natCast, KaehlerDifferential.kerCotangentToTensor_toCotangent, KaehlerDifferential.mvPolynomialBasis_apply, apply_eval_eq, Algebra.PreSubmersivePresentation.jacobiMatrix_naive, derivationToSquareZeroOfLift_apply, Algebra.PreSubmersivePresentation.cotangentComplexAux_apply, Differential.implicitDeriv_C, coe_add, Differential.algHom_deriv, KaehlerDifferential.polynomialEquiv_symm, KaehlerDifferential.tensorKaehlerEquiv_symm_D_tmul', Algebra.Generators.cotangentSpaceBasis_apply, MvPolynomial.IsWeightedHomogeneous.pderiv, KaehlerDifferential.mvPolynomialBasis_repr_D_X, PowerSeries.derivative_exp, LeftInvariantDerivation.coe_derivation, KaehlerDifferential.tensorKaehlerEquiv_symm_D_tmul, Algebra.PreSubmersivePresentation.cotangentComplexAux_zero_iff, KaehlerDifferential.polynomialEquiv_D, mapCoeffs_X, KaehlerDifferential.kerToTensor_apply, PowerSeries.derivative_inv', MvPolynomial.pderiv_one, MvPolynomial.mkDerivation_X, MvPolynomial.pderiv_mul, Polynomial.Bivariate.Polynomial.Bivariate.pderiv_one_equivMvPolynomial, Algebra.Generators.cotangentSpaceBasis_repr_one_tmul, MvPolynomial.pderiv_rename, Polynomial.derivative'_apply, add_apply, DifferentialAlgebra.deriv_algebraMap, leibniz_div, Algebra.SubmersivePresentation.basisKaehlerOfIsCompl_apply, bracket_eq_fun, KaehlerDifferential.kerTotal_eq, Algebra.Generators.H1Cotangent.δAux_C, MvPolynomial.X_mul_pderiv_monomial, Algebra.Extension.CotangentSpace.map_tmul, KaehlerDifferential.span_range_map_derivation_of_isLocalization, mapCoeffs_C, toFun_eq_coe, comp_aeval_eq, neg_apply, instAddMonoidHomClass, leibniz_inv, map_one_eq_zero, KaehlerDifferential.linearMapEquivDerivation_apply_apply, MvPolynomial.pderiv_sumToIter, algebraMap.coe_deriv, mapCoeffs_monomial, Algebra.PreSubmersivePresentation.jacobiMatrix_apply, KaehlerDifferential.span_range_derivation, Algebra.Generators.H1Cotangent.δAux_monomial, Differential.coeff_mapCoeffs, Algebra.Generators.cotangentSpaceBasis_repr_tmul, leibniz_zpow, mk_coe, Algebra.Extension.Hom.sub_one_tmul, Algebra.SubmersivePresentation.linearIndependent_aeval_val_pderiv_relation, MvPolynomial.pderiv_X, Algebra.Generators.H1Cotangent.δAux_toAlgHom, fdifferential_apply, KaehlerDifferential.D_apply, coeFnAddMonoidHom_apply, KaehlerDifferential.ker_map, restrictScalars_apply, MvPolynomial.IsWeightedHomogeneous.sum_weight_X_mul_pderiv, compAlgebraMapL_apply_apply, Polynomial.mkDerivationEquiv_symm_apply, coe_comp, map_zero, KaehlerDifferential.derivationQuotKerTotal_apply, Differential.mapCoeffs_monomial, tensorKaehlerQuotKerSqEquiv_symm_tmul_D, liftKaehlerDifferential_comp_D, Algebra.Generators.H1Cotangent.δAux_ofComp, Differential.mapCoeffs_C, Algebra.Presentation.differentials.comm₂₃', coe_mk', PowerSeries.derivative_invOf, sectionOfRetractionKerToTensorAux_prop, MvPolynomial.derivation_C, tensorKaehlerQuotKerSqEquiv_tmul_D, MvPolynomial.mkDerivation_monomial, derivationToSquareZeroEquivLift_symm_apply_apply_coe, Algebra.PreSubmersivePresentation.aevalDifferential_single, leibniz, map_neg, map_algebraMap, KaehlerDifferential.mvPolynomialBasis_repr_apply, Differential.mapCoeffs_X, smul_apply, Polynomial.Bivariate.pderiv_zero_equivMvPolynomial, MvPolynomial.pderiv_C_mul, leibniz_of_mul_eq_one, Algebra.Generators.toKaehler_tmul_D, coeFn_coe, sectionOfRetractionKerToTensor_algebraMap, Differential.algHom_deriv', coe_smul, MvPolynomial.pderiv_monomial_single, PowerSeries.derivative_coe, MvPolynomial.pderiv_X_of_ne, Polynomial.Bivariate.Polynomial.Bivariate.pderiv_zero_equivMvPolynomial, MvPolynomial.pderiv_monomial, hfdifferential_apply, liftOfDerivationToSquareZero_apply, Polynomial.mkDerivation_X, Polynomial.derivation_ext_iff, KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination, Polynomial.mkDerivation_one_eq_derivative, coe_restrictScalars, Algebra.Generators.repr_CotangentSpaceMap, MvPolynomial.pderiv_pow, map_smul_of_tower, map_aeval, Algebra.Generators.toKaehler_cotangentSpaceBasis, Algebra.SubmersivePresentation.basisKaehler_apply, KaehlerDifferential.polynomial_D_apply, leibniz_pow, Differential.deriv_aeval_eq, MvPolynomial.pderiv_map, Polynomial.derivation_C, map_add, KaehlerDifferential.derivationTensorProduct_algebraMap, MvPolynomial.pderiv_inr_universalFactorizationMap_X, compAEval_eq, tensorProductTo_tmul, derivationOfSectionOfKerSqZero_apply_coe, Differential.logDeriv_eq_zero, map_smul, sectionOfRetractionKerToTensorAux_algebraMap, KaehlerDifferential.mvPolynomialBasis_repr_D, MvPolynomial.pderiv_eq_zero_of_notMem_vars, KaehlerDifferential.ker_map_of_surjective, Algebra.Generators.cotangentRestrict_mk, KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale_symm_D_algebraMap, mapCoeffs_apply, ext_iff, derivationToSquareZeroEquivLift_apply_coe_apply, PowerSeries.coeff_derivative, liftOfDerivationToSquareZero_mk_apply', Differential.implicitDeriv_X, zero_apply, sub_apply, PowerSeries.derivative_subst, Algebra.Extension.Hom.sub_tmul, coe_sub, MvPolynomial.IsHomogeneous.sum_X_mul_pderiv, MvPolynomial.derivation_C_mul, MvPolynomial.aeval_sumElim_pderiv_inl, Differential.algEquiv_deriv', commutator_apply, KaehlerDifferential.mvPolynomialBasis_repr_symm_single, compAlgebraMap_apply, Algebra.IsStandardSmooth.iff_exists_basis_kaehlerDifferential, congr_fun, coe_zero, PowerSeries.derivative_C, KaehlerDifferential.map_D, LeftInvariantDerivation.commutator_coe_derivation, MvPolynomial.pderiv_X_self, KaehlerDifferential.tensorKaehlerEquiv_tmul_D, MvPolynomial.pderiv_C, Polynomial.Bivariate.pderiv_one_equivMvPolynomial, leibniz_invOf, linearEquiv_coe_comp, coe_injective, compAEval_apply, PowerSeries.trunc_derivative, coe_neg, map_sub, KaehlerDifferential.quotKerTotalEquiv_apply, PowerSeries.derivative_inv, PowerSeries.derivative_X, Differential.algEquiv_deriv, MvPolynomial.derivation_ext_iff, Polynomial.mkDerivation_apply, evalAt_apply, MvPolynomial.IsHomogeneous.pderiv, Algebra.SubmersivePresentation.basisDeriv_apply, Algebra.Extension.cotangentComplex_mk, retractionOfSectionOfKerSqZero_tmul_D, KaehlerDifferential.linearCombination_surjective, derivationQuotKerSq_mk, map_intCast, Polynomial.C_smul_derivation_apply, PowerSeries.derivative_pow, MvPolynomial.pderiv_inl_universalFactorizationMap_X, LeftInvariantDerivation.evalAt_apply, apply_aeval_eq, PowerSeries.trunc_derivative'
instInhabited 📖	CompOp	—
instModule 📖	CompOp	33 math math: coe_to_linearMap_comp, LeftInvariantDerivation.left_invariant', LeftInvariantDerivation.left_invariant, linearEquiv_coe_to_linearMap_comp, KaehlerDifferential.quotKerTotalEquiv_symm_comp_D, LieRinehartAlgebra.Hom.anchor_derivation, KaehlerDifferential.polynomialEquiv_comp_D, Polynomial.mkDerivation_one_eq_derivative', KaehlerDifferential.linearMapEquivDerivation_apply_apply, LeftInvariantDerivation.evalAt_coe, KaehlerDifferential.linearMapEquivDerivation_symm_apply, fdifferential_apply, liftKaehlerDifferential_comp, LeftInvariantDerivation.left_invariant'', compAlgebraMapL_apply_apply, Polynomial.mkDerivationEquiv_symm_apply, coe_comp, Polynomial.mkDerivationEquiv_apply, liftKaehlerDifferential_unique_iff, llcomp_apply, fdifferential_comp, KaehlerDifferential.map_compDer, hfdifferential_apply, Polynomial.mkDerivation_X, Polynomial.mkDerivation_one_eq_derivative, KaehlerDifferential.mvPolynomialBasis_repr_comp_D, LeftInvariantDerivation.evalAt_mul, LieRinehartAlgebra.instDerivation, linearEquiv_coe_comp, Polynomial.mkDerivation_apply, evalAt_apply, LieRinehartAlgebra.instLieRinehartRingDerivation, LeftInvariantDerivation.evalAt_apply
instNeg 📖	CompOp	3 math math: coe_neg_linearMap, neg_apply, coe_neg
instSMul 📖	CompOp	7 math math: LeftInvariantDerivation.lift_smul, instIsScalarTower, smul_apply, instIsCentralScalar, coe_smul, instSMulCommClass, coe_smul_linearMap
instSub 📖	CompOp	3 math math: coe_sub_linearMap, sub_apply, coe_sub
instZero 📖	CompOp	4 math math: LeftInvariantDerivation.lift_zero, zero_apply, coe_zero_linearMap, coe_zero
liftOfRightInverse 📖	CompOp	2 math math: liftOfRightInverse_apply, liftOfRightInverse_eq
liftOfSurjective 📖	CompOp	1 math math: liftOfSurjective_apply
llcomp 📖	CompOp	1 math math: llcomp_apply
mk' 📖	CompOp	2 math math: coe_mk'_linearMap, coe_mk'
restrictScalars 📖	CompOp	3 math math: restrictScalars_apply, KaehlerDifferential.map_compDer, coe_restrictScalars
toLinearMap 📖	CompOp	16 math math: coe_to_linearMap_comp, linearEquiv_coe_to_linearMap_comp, toFun_eq_coe, coe_neg_linearMap, leibniz', commutator_coe_linear_map, coe_mk'_linearMap, coe_comp, coeFn_coe, map_one_eq_zero', coe_sub_linearMap, coe_add_linearMap, coe_smul_linearMap, coe_zero_linearMap, linearEquiv_coe_comp, LeftInvariantDerivation.toFun_eq_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_apply 📖	mathematical	—	DFunLike.coe Derivation instFunLike instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	—
coeFnAddMonoidHom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom Derivation AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid Pi.addZeroClass AddMonoidHom.instFunLike coeFnAddMonoidHom instFunLike	—	—
coeFn_coe 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LinearMap.instFunLike toLinearMap Derivation instFunLike	—	—
coe_add 📖	mathematical	—	DFunLike.coe Derivation instFunLike instAdd Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	—
coe_add_linearMap 📖	mathematical	—	toLinearMap Derivation instAdd LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LinearMap.instAdd	—	—
coe_comp 📖	mathematical	—	DFunLike.coe Derivation instFunLike LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring instAddCommMonoid instModule IsScalarTower.to_smulCommClass smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike LinearMap.compDer NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LinearMap.comp RingHomCompTriple.ids LinearMap.restrictScalars LinearMap.IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Algebra.toSMul toLinearMap	—	IsScalarTower.to_smulCommClass smulCommClass_self
coe_injective 📖	mathematical	—	Derivation DFunLike.coe instFunLike	—	DFunLike.coe_injective
coe_mk' 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddCancelCommMonoid.toAddCommMonoid Algebra.toModule LinearMap.instFunLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	Derivation instFunLike mk'	—	—
coe_mk'_linearMap 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddCancelCommMonoid.toAddCommMonoid Algebra.toModule LinearMap.instFunLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	toLinearMap mk'	—	—
coe_neg 📖	mathematical	—	DFunLike.coe Derivation CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike instNeg Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
coe_neg_linearMap 📖	mathematical	—	toLinearMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Derivation instNeg LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LinearMap.instNeg	—	—
coe_restrictScalars 📖	mathematical	—	DFunLike.coe Derivation instFunLike restrictScalars	—	—
coe_smul 📖	mathematical	—	DFunLike.coe Derivation instFunLike instSMul Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	—
coe_smul_linearMap 📖	mathematical	—	toLinearMap Derivation instSMul LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LinearMap.instSMul DistribMulAction.toDistribSMul AddCommMonoid.toAddMonoid	—	—
coe_sub 📖	mathematical	—	DFunLike.coe Derivation CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike instSub Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	—
coe_sub_linearMap 📖	mathematical	—	toLinearMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Derivation instSub LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LinearMap.instSub	—	—
coe_to_linearMap_comp 📖	mathematical	—	toLinearMap DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Derivation instAddCommMonoid instModule IsScalarTower.to_smulCommClass smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike LinearMap.compDer LinearMap.comp NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule RingHomCompTriple.ids LinearMap.restrictScalars LinearMap.IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Algebra.toSMul	—	IsScalarTower.to_smulCommClass smulCommClass_self
coe_zero 📖	mathematical	—	DFunLike.coe Derivation instFunLike instZero Pi.instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
coe_zero_linearMap 📖	mathematical	—	toLinearMap Derivation instZero LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LinearMap.instZero	—	—
compAlgebraMapL_apply_apply 📖	mathematical	—	DFunLike.coe Derivation instFunLike LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring instAddCommMonoid instModule IsScalarTower.to_smulCommClass smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction IsScalarTower.to_smulCommClass' LinearMap.instFunLike compAlgebraMapL RingHom RingHom.instFunLike algebraMap	—	IsScalarTower.to_smulCommClass smulCommClass_self IsScalarTower.to_smulCommClass'
compAlgebraMap_apply 📖	mathematical	—	DFunLike.coe Derivation instFunLike compAlgebraMap RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	—
congr_fun 📖	mathematical	—	DFunLike.coe Derivation instFunLike	—	DFunLike.congr_fun
eqOn_adjoin 📖	mathematical	Set.EqOn DFunLike.coe Derivation instFunLike	SetLike.coe Subalgebra CommSemiring.toSemiring Subalgebra.instSetLike Algebra.adjoin	—	Algebra.adjoin_induction map_algebraMap map_add AddMonoidHomClass.toAddHomClass instAddMonoidHomClass leibniz
ext 📖	—	DFunLike.coe Derivation instFunLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe Derivation instFunLike	—	ext
ext_of_adjoin_eq_top 📖	—	Algebra.adjoin CommSemiring.toSemiring Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Set.EqOn DFunLike.coe Derivation instFunLike	—	—	ext eqOn_adjoin
instAddMonoidHomClass 📖	mathematical	—	AddMonoidHomClass Derivation AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring AddCommMonoid.toAddMonoid instFunLike	—	AddHom.map_add' LinearMap.map_zero
instIsCentralScalar 📖	mathematical	—	IsCentralScalar Derivation instSMul MulOpposite MulOpposite.instMonoid SMulCommClass.op_right SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction SMulCommClass.op_left	—	SMulCommClass.op_right SMulCommClass.op_left ext IsCentralScalar.op_smul_eq_smul
instIsScalarTower 📖	mathematical	—	IsScalarTower Derivation instSMul	—	ext smul_assoc
instSMulCommClass 📖	mathematical	—	SMulCommClass Derivation instSMul	—	ext SMulCommClass.smul_comm
leibniz 📖	mathematical	—	DFunLike.coe Derivation instFunLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	leibniz'
leibniz' 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LinearMap.instFunLike toLinearMap Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	—
leibniz_div 📖	mathematical	—	DFunLike.coe Derivation CommRing.toCommSemiring Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid instFunLike DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Module.toDistribMulAction Monoid.toNatPow InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero SubNegMonoid.toSub	—	div_eq_mul_inv leibniz leibniz_inv inv_pow neg_smul smul_neg smul_smul add_comm sub_eq_add_neg smul_add inv_mul_mul_self inv_inv Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_inv_one Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one add_zero Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero
leibniz_div_const 📖	mathematical	DFunLike.coe Derivation CommRing.toCommSemiring Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Module.toDistribMulAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero	—	leibniz_div inv_pow smul_zero sub_zero smul_smul mul_self_mul_inv inv_inv Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_inv_one Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one add_zero Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add
leibniz_inv 📖	mathematical	—	DFunLike.coe Derivation CommRing.toCommSemiring Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid instFunLike InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Module.toDistribMulAction NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing Monoid.toNatPow	—	eq_or_ne inv_zero map_zero AddMonoidHomClass.toZeroHomClass instAddMonoidHomClass zero_pow Nat.instCharZero Nat.instAtLeastTwoHAddOfNat neg_zero smul_zero leibniz_of_mul_eq_one inv_mul_cancel₀
leibniz_invOf 📖	mathematical	—	DFunLike.coe Derivation CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike Invertible.invOf Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup Monoid.toNatPow	—	leibniz_of_mul_eq_one invOf_mul_self
leibniz_of_mul_eq_one 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	DFunLike.coe Derivation CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup Monoid.toNatPow	—	neg_smul eq_neg_of_add_eq_zero_left sq smul_smul one_smul leibniz smul_add add_comm map_one_eq_zero smul_zero
leibniz_pow 📖	mathematical	—	DFunLike.coe Derivation instFunLike Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring AddMonoid.toNatSMul AddCommMonoid.toAddMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction	—	pow_zero map_one_eq_zero zero_smul LE.le.eq_or_lt zero_le Nat.instCanonicallyOrderedAdd zero_add pow_one tsub_self Nat.instOrderedSub one_smul pow_succ' leibniz SMulCommClass.smul_comm AddMonoid.nat_smulCommClass' smul_smul add_zero add_smul one_nsmul
leibniz_zpow 📖	mathematical	—	DFunLike.coe Derivation CommRing.toCommSemiring Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid instFunLike DivInvMonoid.toZPow DivisionRing.toDivInvMonoid Field.toDivisionRing SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Module.toDistribMulAction	—	zpow_zero map_one_eq_zero zero_sub zpow_neg zpow_one zero_smul zero_zpow map_zero AddMonoidHomClass.toZeroHomClass instAddMonoidHomClass smul_zero zpow_natCast leibniz_pow natCast_zsmul leibniz_inv inv_pow pow_mul Nat.cast_smul_eq_nsmul Int.cast_smul_eq_zsmul smul_smul Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_inv_one Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg mul_one Mathlib.Tactic.RingNF.mul_assoc_rev add_zero Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf zpow_sub₀ Int.natCast_natAbs
liftOfRightInverse_apply 📖	mathematical	DFunLike.coe Derivation CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring Algebra.toModule instFunLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	liftOfRightInverse	—	map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass sub_self instAddMonoidHomClass
liftOfRightInverse_eq 📖	mathematical	DFunLike.coe	liftOfRightInverse	—	ext liftOfRightInverse_apply
liftOfSurjective_apply 📖	mathematical	DFunLike.coe Derivation CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule CommSemiring.toSemiring Algebra.toModule instFunLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	liftOfSurjective	—	liftOfRightInverse_apply
linearEquiv_coe_comp 📖	mathematical	—	DFunLike.coe Derivation instFunLike LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instAddCommMonoid instModule IsScalarTower.to_smulCommClass smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.compDer LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LinearMap.instFunLike LinearMap.comp RingHomCompTriple.ids LinearMap.restrictScalars LinearMap.IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Algebra.toSMul LinearEquiv.toLinearMap toLinearMap	—	RingHomInvPair.ids IsScalarTower.to_smulCommClass smulCommClass_self
linearEquiv_coe_to_linearMap_comp 📖	mathematical	—	toLinearMap DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Derivation instAddCommMonoid instModule IsScalarTower.to_smulCommClass smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.compDer LinearMap.comp NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule RingHomCompTriple.ids LinearMap.restrictScalars LinearMap.IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Algebra.toSMul LinearEquiv.toLinearMap	—	RingHomInvPair.ids IsScalarTower.to_smulCommClass smulCommClass_self
llcomp_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Derivation instAddCommMonoid instModule IsScalarTower.to_smulCommClass smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.addCommMonoid LinearMap.module instSMulCommClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearMap.instFunLike llcomp LinearMap.compDer	—	IsScalarTower.to_smulCommClass smulCommClass_self instSMulCommClass
map_add 📖	mathematical	—	DFunLike.coe Derivation instFunLike Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	map_add AddMonoidHomClass.toAddHomClass instAddMonoidHomClass
map_aeval 📖	mathematical	—	DFunLike.coe Derivation instFunLike AlgHom Polynomial CommSemiring.toSemiring Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.module Semiring.toModule LinearMap.instFunLike Polynomial.derivative	—	Polynomial.induction_on Polynomial.aeval_C map_algebraMap Polynomial.derivative_C map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass zero_smul map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AddMonoidHomClass.toAddHomClass instAddMonoidHomClass Polynomial.derivative_add add_smul map_mul NonUnitalAlgSemiHomClass.toMulHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass Polynomial.aeval_X leibniz leibniz_pow add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.cast_smul_eq_nsmul Nat.cast_add Nat.cast_one smul_zero add_zero Polynomial.derivative_mul MulZeroClass.zero_mul Polynomial.derivative_X_pow_succ RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_natCast map_one MonoidHomClass.toOneHomClass zero_add SemigroupAction.mul_smul
map_algebraMap 📖	mathematical	—	DFunLike.coe Derivation instFunLike RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	mul_one map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass Algebra.smul_def map_smul map_one_eq_zero smul_zero
map_intCast 📖	mathematical	—	DFunLike.coe Derivation CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	zsmul_one map_smul_of_tower LinearMap.CompatibleSMul.intModule map_one_eq_zero smul_zero
map_natCast 📖	mathematical	—	DFunLike.coe Derivation instFunLike AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	nsmul_one map_smul_of_tower LinearMap.IsScalarTower.compatibleSMul AddCommMonoid.nat_isScalarTower map_one_eq_zero smul_zero
map_neg 📖	mathematical	—	DFunLike.coe Derivation CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing	—	map_neg instAddMonoidHomClass
map_one_eq_zero 📖	mathematical	—	DFunLike.coe Derivation instFunLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	map_one_eq_zero'
map_one_eq_zero' 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LinearMap.instFunLike toLinearMap AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
map_smul 📖	mathematical	—	DFunLike.coe Derivation instFunLike Algebra.toSMul CommSemiring.toSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	LinearMap.map_smul
map_smul_of_tower 📖	mathematical	—	DFunLike.coe Derivation instFunLike	—	LinearMap.map_smul_of_tower
map_sub 📖	mathematical	—	DFunLike.coe Derivation CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing AddCommGroup.toAddGroup	—	map_sub instAddMonoidHomClass
map_zero 📖	mathematical	—	DFunLike.coe Derivation instFunLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	map_zero AddMonoidHomClass.toZeroHomClass instAddMonoidHomClass
mk_coe 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LinearMap.instFunLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	Derivation instFunLike	—	—
neg_apply 📖	mathematical	—	DFunLike.coe Derivation CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
restrictScalars_apply 📖	mathematical	—	DFunLike.coe Derivation instFunLike restrictScalars	—	—
smul_apply 📖	mathematical	—	DFunLike.coe Derivation instFunLike instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	—
sub_apply 📖	mathematical	—	DFunLike.coe Derivation CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instFunLike instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	—
toFun_eq_coe 📖	mathematical	—	AddHom.toFun AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring LinearMap.toAddHom RingHom.id Algebra.toModule toLinearMap DFunLike.coe Derivation instFunLike	—	—
zero_apply 📖	mathematical	—	DFunLike.coe Derivation instFunLike instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—

Derivation.Simps

Definitions

Name	Category	Theorems
apply 📖	CompOp	—

LinearEquiv

Definitions

Name	Category	Theorems
compDer 📖	CompOp	3 math math: Derivation.linearEquiv_coe_to_linearMap_comp, KaehlerDifferential.polynomialEquiv_comp_D, Derivation.linearEquiv_coe_comp

LinearMap

Definitions

Name	Category	Theorems
compDer 📖	CompOp	8 math math: Derivation.coe_to_linearMap_comp, KaehlerDifferential.quotKerTotalEquiv_symm_comp_D, Derivation.liftKaehlerDifferential_comp, Derivation.coe_comp, Derivation.liftKaehlerDifferential_unique_iff, Derivation.llcomp_apply, KaehlerDifferential.map_compDer, KaehlerDifferential.mvPolynomialBasis_repr_comp_D

---

← Back to Index