| Name | Category | Theorems |
|---|
applyModule 📖 | CompOp | 22 mathmath: smul_def, apply_smulCommClass', Module.AEval'.X_smul_of, ringHomEndFinsupp_apply_apply, Module.AEval'.of_symm_X_smul, QuadraticMap.associated_apply, Module.AEval'.X_pow_smul_of, QuadraticMap.associated_toQuadraticMap, ringEquivEndFinsupp_apply_apply_apply, apply_smulCommClass, jacobson_density, Polynomial.span_minpoly_eq_annihilator, Module.AEval'_def, Module.Finite.toModuleEnd_moduleEnd_surjective, apply_faithfulSMul, ringEquivEndFinsupp_apply_apply_support, Projectivization.generalLinearGroup_smul_def, apply_isScalarTower, ringEquivEndFinsupp_symm_apply_apply, ringHomEndFinsupp_surjective, Module.instFinitePolynomialAEval', LinearMap.instIsSimpleModuleEndOfNontrivial
|
instMonoid 📖 | CompOp | 177 mathmath: pow_apply_mem_of_forall_mem, LinearMap.pow_mulRight, exists_ker_pow_eq_ker_pow_succ, Matrix.UnitaryGroup.toGL_mul, smul_def, LieModule.toEnd_pow_apply_map, isNilpotent_restrict_genEigenspace_nat, IsNilpotent.mapQ, HasUnifEigenvector.pow_apply, LinearMap.GeneralLinearGroup.congrLinearEquiv_refl, iterate_succ', Representation.asGroupHom_apply, LieModule.exists_genWeightSpace_zero_le_ker_of_isNoetherian, id_pow, LieModule.isNilpotent_toEnd_genWeightSpace_zero, LinearMap.charpoly_nilpotent_tfae, LinearMap.isUnit_iff_range_eq_top, Matrix.GeneralLinearGroup.coe_toLin, IsLocalizedModule.iso_apply_mk, apply_smulCommClass', LinearMap.eventually_iSup_ker_pow_eq, LinearMap.GeneralLinearGroup.generalLinearEquiv_to_linearMap, SpecialLinearGroup.mem_range_toGeneralLinearGroup_iff, AlgEquiv.pow_toLinearMap, LinearMap.isUnit_iff_isUnit_det, LieModule.mem_posFittingCompOf, LocalizedModule.lift'_mk, LieModule.isNilpotent_toEnd_of_isNilpotent, Submodule.mapQ_pow, pow_restrict, ModularGroup.lcRow0Extend_symm_apply, HasEigenvalue.pow, AffineEquiv.linear_equivUnitsAffineMap_symm_apply, LinearMap.isUnit_iff_ker_eq_bot, Matrix.isNilpotent_toLin'_iff, QuadraticMap.associated_apply, LieModule.mem_genWeightSpace, LinearMap.isCompl_iSup_ker_pow_iInf_range_pow, LinearMap.baseChange_pow, isUnit_inv_apply_apply_of_isUnit, LinearMap.GeneralLinearGroup.ofLinearEquiv_inv, Matrix.toLpLin_symm_pow, IsTensorProduct.map_pow, algebraMap_isUnit_inv_apply_eq_iff', LieModule.exists_genWeightSpace_le_ker_of_isNoetherian, LieModule.coe_genWeightSpaceOf_zero, isNilpotent_iff_of_finite, ker_pow_eq_ker_pow_finrank_of_le, LieSubalgebra.coe_ad_pow, isLocalizedModule_iff, LinearMap.pow_eq_aeval_mod_charpoly, Matrix.toLpLin_pow, Module.AEval'.X_pow_smul_of, Matrix.isUnit_toLin'_iff, pow_apply, ModularGroup.lcRow0Extend_apply, LinearMap.isNilpotent_toMatrix_iff, IsSemisimple.pow, LinearMap.charpoly_eq_X_pow_iff, LinearMap.GeneralLinearGroup.toLinearEquiv_inv, LieAlgebra.ad_nilpotent_of_nilpotent, Matrix.toLin_pow, fwdDiff_aux.shiftₗ_pow_apply, Matrix.GeneralLinearGroup.toLin'_apply, LieAlgebra.ad_pow_lie, coe_pow, QuadraticMap.associated_toQuadraticMap, LieModule.isNilpotent_toEnd_of_isNilpotent₂, LinearMap.ker_noncommProd_eq_of_supIndep_ker, LieSubmodule.mapsTo_pow_toEnd_sub_algebraMap, IsLocalizedModule.fromLocalizedModule_mk, ContinuousLinearMap.isUnit_iff_isUnit_toLinearMap, isUnit_iff, submodule_pow_eq_zero_of_pow_eq_zero, pow_mulLeftLinearMap, LieModule.exists_forall_pow_toEnd_eq_zero, LinearMap.iterateKer_coe, pow_mulRightLinearMap, Matrix.UnitaryGroup.coe_toGL, LinearMap.GeneralLinearGroup.congrLinearEquiv_apply, Polynomial.linearIndependent_powers_iff_aeval, LieSubalgebra.mem_engel_iff, ContinuousLinearMap.coe_pow, Matrix.isUnit_toLin_iff, mem_genEigenspace_top, Matrix.toLin'_pow, iterate_surjective, IsSl2Triple.HasPrimitiveVectorWith.pow_toEnd_f_eq_zero_of_eq_nat, LieModule.isNilpotent_toEnd_of_mem_rootSpace, isNilpotent_restrict_maxGenEigenspace_sub_algebraMap, LieSubalgebra.isNilpotent_ad_of_isNilpotent_ad, LinearMap.isNilpotent_iff_charpoly, LieAlgebra.toEnd_pow_apply_mem, LinearMap.isNilpotent_mulRight_iff, mem_iInf_maxGenEigenspace_iff, LinearMap.eventually_isCompl_ker_pow_range_pow, eventually_disjoint_ker_pow_range_pow, exists_isNilpotent_isSemisimple_of_separable_of_dvd_pow, IsSl2Triple.HasPrimitiveVectorWith.lie_f_pow_toEnd_f, LinearMap.isUnit_toMatrix'_iff, LieModule.toEnd_pow_lie, apply_smulCommClass, LocalizedModule.lift_mk, LinearMap.GeneralLinearGroup.coe_ofLinearEquiv, genEigenspace_zero_nat, HasUnifEigenvalue.pow, genEigenrange_nat, LinearMap.GeneralLinearGroup.coe_toLinearEquiv, LinearMap.eventually_iInf_range_pow_eq, LieModule.isNilpotent_iff_forall, SpecialLinearGroup.toGeneralLinearGroup_injective, LieModule.isNilpotent_toEnd_sub_algebraMap, LinearMap.isUnit_toMatrix_iff, IsSl2Triple.HasPrimitiveVectorWith.lie_e_pow_succ_toEnd_f, IsSl2Triple.HasPrimitiveVectorWith.lie_h_pow_toEnd_f, LinearMap.GeneralLinearGroup.congrLinearEquiv_symm, isNilpotent_restrict_sub_algebraMap, apply_faithfulSMul, pow_map_zero_of_le, LieAlgebra.isNilpotent_ad_of_mem_rootSpace, AlgebraicGeometry.tilde.isUnit_algebraMap_end_basicOpen, mem_maxGenEigenspace, Polynomial.aeval_endomorphism, LinearMap.iterateRange_coe, commute_pow_left_of_commute, Algebra.lmul_isUnit_iff, SpecialLinearGroup.toGeneralLinearGroup_toLinearEquiv_apply, genEigenspace_nat, LinearMap.GeneralLinearGroup.congrLinearEquiv_trans', LieModule.isNilpotent_iff_forall', IsLocalizedModule.fromLocalizedModule'_mk, LinearMap.GeneralLinearGroup.toLinearEquiv_mul, mem_genEigenspace_nat, LieSubmodule.coe_toEnd_pow, LieModule.mem_genWeightSpaceOf, isUnit_intrinsicStar_iff, mulSemiringActionToAlgEquiv_conjAct_surjective, SpecialLinearGroup.coe_toGeneralLinearGroup_apply, IsLocalizedModule.map_units, isNilpotent_restrict_of_le, LieAlgebra.nilpotent_ad_of_nilpotent_algebra, isUnit_apply_inv_apply_of_isUnit, LinearMap.eventually_codisjoint_ker_pow_range_pow, isNilpotent_restrict_genEigenspace_top, LinearMap.trace_conj, LinearMap.lTensor_pow, LinearMap.GeneralLinearGroup.congrLinearEquiv_trans, Projectivization.generalLinearGroup_smul_def, LieAlgebra.mem_zeroRootSubalgebra, ker_pow_le_ker_pow_finrank, LinearMap.GeneralLinearGroup.ofLinearEquiv_mul, apply_isScalarTower, Matrix.UnitaryGroup.toGL_one, isNilpotent.restrict, LinearMap.pow_mulLeft, LinearMap.toMatrix_pow, fwdDiff_aux.coe_fwdDiffₗ_pow, iterate_bijective, ker_pow_constant, LieAlgebra.isNilpotent_iff_forall, mem_genEigenspace, LinearMap.rTensor_pow, LieAlgebra.isNilpotent_ad_of_isNilpotent, TensorProduct.map_pow, iterate_succ, HasEigenvector.pow_apply, PiTensorProduct.map_pow, LinearMap.GeneralLinearGroup.coeFn_generalLinearEquiv, iterate_injective, IsUnit.intrinsicStar, exists_isNilpotent_isSemisimple, LinearMap.isNilpotent_mulLeft_iff, algebraMap_isUnit_inv_apply_eq_iff, Matrix.GeneralLinearGroup.toLin_apply, LieModule.toEnd_pow_comp_lieHom, LinearMap.IsSymmetric.pow, Submodule.le_comap_pow_of_le_comap
|
instMul 📖 | CompOp | 92 mathmath: LinearMap.toMatrixAlgEquiv'_mul, FDRep.endRingEquiv_symm_comp_ρ, LinearMap.IsIdempotentElem.commute_iff, LinearMap.toMatrixOrthonormal_reindex, Representation.IntertwiningMap.coe_mul, LinearMap.trace_mul_cycle, mul_eq_comp, ContinuousLinearMap.IsIdempotentElem.toLinearMap, IsSemisimple.mul_of_commute, ModuleCat.endRingEquiv_symm_apply_hom, LinearMap.toMatrixOrthonormal_apply_apply, IsSimpleRing.exists_ringEquiv_matrix_end_mulOpposite, LinearMap.commute_mulLeft_right, LinearEquiv.coe_toLinearMap_mul, LinearMap.isIdempotentElem_iff_eq_isCompl_projection_range_ker, LinearMap.IsSymmetricProjection.isIdempotentElem, LinearMap.isIdempotentElem_map_one_iff, RingEquiv.moduleEndSelf_symm_apply, LinearMap.restrict_commute, LinearMap.trace_mul_comm, QuadraticMap.associated_apply, LinearMap.isSymmetric_adjoint_mul_self, LinearMap.mul_eq_one_comm, RingEquiv.moduleEndSelfOp_apply, Rep.RepToAction_map_hom, ContinuousLinearMap.isIdempotentElem_toLinearMap_iff, QuadraticMap.associated_toQuadraticMap, LinearMap.toMatrixOrthonormal_symm_apply, ringEquivEndFinsupp_apply_apply_apply, RingEquiv.moduleEndSelf_apply, LinearMap.IsIdempotentElem.commute_iff_of_isUnit, coe_mul, LinearEquiv.conjRingEquiv_apply_apply, addMonoidEndRingEquivInt_apply, LinearMap.lTensor_mul, PiTensorProduct.map_mul, LinearMap.toMatrix'_mul, mem_center_iff, LinearMap.re_inner_adjoint_mul_self_nonneg, Submodule.isIdempotentElemEquiv_apply_coe, LinearMap.toMatrix_mul, LinearMap.isIdempotentElem_apply_one_iff, QuadraticMap.half_moduleEnd_apply_eq_half_smul, mem_subsemigroupCenter_iff, LinearMap.toMatrixOrthonormal_apply, Submodule.isIdempotentElemEquiv_symm_apply_coe, TensorProduct.map_mul, commute_id_right, LinearMap.IsProj.isIdempotentElem, LinearEquiv.ofInjectiveEndo_right_inv, TensorProduct.AlgebraTensorModule.lTensor_mul, IsSemisimpleModule.exists_end_ringEquiv, LinearMap.mul_eq_one_of_mul_eq_one, TensorProduct.AlgebraTensorModule.map_mul, LinearMap.isSymmetricProjection_iff, LieModule.commute_toEnd_of_mem_center_right, IsSemisimpleModule.exists_end_ringEquiv_pi_matrix_divisionRing, TensorProduct.AlgebraTensorModule.rTensor_mul, Rep.RepToAction_obj_ρ, LinearMap.isProj_range_iff_isIdempotentElem, IsSemisimpleRing.exists_ringEquiv_pi_matrix_end_mulOpposite, LinearEquiv.conjRingEquiv_symm_apply_apply, LinearMap.isStarProjection_toContinuousLinearMap_iff, FDRep.of_ρ, LinearEquiv.ofInjectiveEndo_left_inv, ringEquivEndFinsupp_apply_apply_support, LinearMap.trace_conj, Matrix.Represents.mul, Rep.RepToAction_obj, LinearMap.isStarProjection_iff_isSymmetricProjection, mul_apply, LieAlgebra.commute_ad_of_commute, ContinuousLinearMap.coe_mul, addMonoidEndRingEquivInt_symm_apply, ModuleCat.endRingEquiv_apply, IsTensorProduct.map_mul, Submodule.IsCompl.projection_isIdempotentElem, LinearMap.toMatrixAlgEquiv_mul, ringEquivEndFinsupp_symm_apply_apply, LinearMap.baseChange_mul, LinearMap.IsAdjointPair.mul, LinearMap.trace_mul_cycle', LinearMap.prodMap_mul, LieModule.commute_toEnd_of_mem_center_left, LinearMap.toSpanSingleton_isIdempotentElem_iff, IsSemisimpleModule.exists_end_ringEquiv_pi_matrix_end, LinearMap.rTensor_mul, FDRep.endRingEquiv_comp_ρ, commute_id_left, RingEquiv.moduleEndSelfOp_symm_apply, LinearMap.isProj_iff_isIdempotentElem, LinearMap.IsSymmetric.mul_of_commute
|
instOne 📖 | CompOp | 57 mathmath: LinearMap.prodMap_one, isNilpotent_restrict_genEigenspace_nat, Subspace.dualRestrict_comp_dualLift, LinearMap.toMatrix_one, one_eq_id, TensorProduct.AlgebraTensorModule.rTensor_one, LinearMap.ringLmapEquivSelf_symm_apply, maxGenEigenspace_eq_maxGenEigenspace_zero, LinearMap.baseChange_one, LinearMap.trace_one, QuadraticMap.associated_apply, LieModule.mem_genWeightSpace, LinearMap.mul_eq_one_comm, LinearMap.exists_eq_smul_id_of_forall_notLinearIndependent, LinearMap.IsIdempotentElem.range_eq_ker_one_sub, QuadraticMap.associated_toQuadraticMap, LinearMap.isAdjointPair_one, IsTensorProduct.map_one, invtSubmodule.one, mem_genEigenspace_top, genEigenspace_one, PiTensorProduct.map_one, TensorProduct.map_one, QuadraticMap.half_moduleEnd_apply_eq_half_smul, TensorProduct.AlgebraTensorModule.map_one, eigenspace_def, one_apply, mem_iInf_maxGenEigenspace_iff, LinearEquiv.ofInjectiveEndo_right_inv, AlgEquiv.one_toLinearMap, IsBaseChange.endHom_one, LinearMap.mul_eq_one_of_mul_eq_one, genEigenrange_nat, LinearMap.charpoly_one, LinearMap.exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent, Matrix.Represents.one, LinearMap.charpoly_sub_smul, LinearMap.restrict_smul_one, mem_maxGenEigenspace, genEigenspace_div, Matrix.cramer_one, TensorProduct.AlgebraTensorModule.lTensor_one, genEigenspace_nat, mem_genEigenspace_nat, LieModule.mem_genWeightSpaceOf, LinearEquiv.ofInjectiveEndo_left_inv, isNilpotent_restrict_genEigenspace_top, LinearMap.commute_transvections_iff_of_basis, LinearMap.toMatrix'_one, LinearMap.IsIdempotentElem.ker_eq_range_one_sub, mem_genEigenspace, ContinuousLinearMap.coe_one, LinearMap.tendsto_birkhoffAverage_of_ker_subset_closure, LinearMap.isPositive_one, LinearMap.exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent_of_basis, coe_one, ZLattice.comap_refl
|
instRing 📖 | CompOp | 159 mathmath: exp_mul_of_derivation, RootPairing.four_nsmul_coPolarization_compl_polarization_apply_root, LinearMap.BilinForm.isSkewAdjoint_bracket, HasEigenvalue.mem_spectrum, LieModule.toEnd_pow_apply_map, Matrix.spectrum_toEuclideanLin, LieModule.trace_toEnd_eq_zero_of_mem_lcs, LieAlgebra.mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace, LieAlgebra.finrank_engel, skewAdjointLieSubalgebraEquiv_apply, spectrum_intrinsicStar, Matrix.spectrum_toLpLin, LieAlgebra.isRegular_iff_natTrailingDegree_charpoly_eq_rank, LieModule.exists_genWeightSpace_zero_le_ker_of_isNoetherian, LieSubalgebra.toEnd_eq, LieModule.isNilpotent_toEnd_genWeightSpace_zero, minpoly_algHom_toLinearMap, intCast_apply, skewAdjointLieSubalgebraEquiv_symm_apply, LinearMap.spectrum_toMatrix', LieModule.trace_toEnd_genWeightSpace, LieModule.shiftedGenWeightSpace.toEnd_eq, LieAlgebra.ad_isSemisimple_of_isSemisimple, instLieModule, LieSubmodule.Quotient.toEnd_comp_mk', LieModule.instIsTriangularizableSubtypeEndMemLieSubalgebraRangeToEnd, LieModule.mem_posFittingCompOf, LieModule.isNilpotent_range_toEnd_iff, LieAlgebra.rank_le_natTrailingDegree_charpoly_ad, LieSubmodule.lie_top_eq_of_span_sup_eq_top, LieAlgebra.ad_eq_lmul_left_sub_lmul_right, LieModule.isNilpotent_toEnd_of_isNilpotent, LieAlgebra.hasCentralRadical_and_of_isIrreducible_of_isFaithful, LieSubmodule.coe_map_toEnd_le, QuadraticMap.associated_apply, LieModule.mem_genWeightSpace, LieSubalgebra.toEnd_mk, intCast_def, LieModule.exists_genWeightSpace_le_ker_of_isNoetherian, hasUnifEigenvalue_iff_mem_spectrum, LieModule.coe_genWeightSpaceOf_zero, LieAlgebra.engel_isBot_of_isMin.lieCharpoly_map_eval, LieSubmodule.traceForm_eq_zero_of_isTrivial, lieEquivMatrix'_apply, LieModule.weight_vector_multiplication, LieDerivation.exp_map_apply, LinearMap.minpoly_toMatrix', LieSubalgebra.coe_ad_pow, RootPairing.GeckConstruction.trace_toEnd_eq_zero, LieModule.lie_mem_maxGenEigenspace_toEnd, LieModule.IsTriangularizable.maxGenEigenspace_eq_top, LieSubmodule.trace_eq_trace_restrict_of_le_idealizer, LieModule.isFaithful_iff, LieSubmodule.toEnd_comp_subtype_mem, LinearMap.minpoly_dvd_charpoly, LieAlgebra.ad_nilpotent_of_nilpotent, LieModule.rank_eq_natTrailingDegree, LieDerivation.exp_apply, LieAlgebra.trace_toEnd_eq_zero, LieAlgebra.ad_pow_lie, QuadraticMap.associated_toQuadraticMap, LinearMap.isPositive_natCast, LieModule.isNilpotent_toEnd_of_isNilpotent₂, LieSubmodule.mapsTo_pow_toEnd_sub_algebraMap, Derivation.commutator_coe_linear_map, LieModule.exists_forall_pow_toEnd_eq_zero, JacobsonNoether.exist_pow_eq_zero_of_le, LieSubmodule.toEnd_restrict_eq_toEnd, LieModule.IsFaithful.injective_toEnd, LieModule.trace_comp_toEnd_genWeightSpace_eq, lie_apply, killingForm_apply_apply, LinearMap.spectrum_toMatrix, LieSubalgebra.mem_engel_iff, LinearMap.IsSymmetric.natCast, LieModule.iterate_toEnd_mem_lowerCentralSeries₂, LinearMap.hasEigenvalue_zero_tfae, Matrix.minpoly_toLin', IsSl2Triple.HasPrimitiveVectorWith.pow_toEnd_f_eq_zero_of_eq_nat, LieModule.toEnd_eq_iff, LinearEquiv.lieConj_apply, LieModule.isNilpotent_toEnd_of_mem_rootSpace, LieDerivation.toLinearMapLieHom_injective, commute_exp_left_of_commute, LieModule.toEnd_lie, isRoot_of_hasEigenvalue, LinearMap.minpoly_toMatrix, LieSubalgebra.isNilpotent_ad_of_isNilpotent_ad, LieAlgebra.ad_apply, LieAlgebra.toEnd_pow_apply_mem, LieAlgebra.conj_ad_apply, IsSemisimpleRing.moduleEnd, finite_spectrum, LieModule.isRegular_iff_natTrailingDegree_charpoly_eq_rank, IsSl2Triple.HasPrimitiveVectorWith.lie_f_pow_toEnd_f, LieDerivation.commutator_coe_linear_map, Matrix.spectrum_toLin, LieModule.toEnd_pow_lie, LieSubmodule.coe_toEnd, LieModule.toEnd_apply_apply, LieModule.commute_toEnd_of_mem_center_right, LieModule.toEnd_baseChange, Polynomial.span_minpoly_eq_annihilator, LieModule.isNilpotent_iff_forall, LieModule.isNilpotent_toEnd_sub_algebraMap, lieEquivMatrix'_symm_apply, IsSl2Triple.HasPrimitiveVectorWith.lie_e_pow_succ_toEnd_f, IsSl2Triple.HasPrimitiveVectorWith.lie_h_pow_toEnd_f, FiniteField.minpoly_frobeniusAlgHom, ContinuousLinearMap.spectrum_eq, hasEigenvalue_iff_isRoot, minpoly_algEquiv_toLinearMap, LieAlgebra.IsKilling.cartanEquivDual_apply_apply, LieModule.toEnd_eq_zero_iff, LieAlgebra.isNilpotent_ad_of_mem_rootSpace, isIntegral, LieModule.traceForm_apply_apply, LieAlgebra.IsKilling.isSemisimple_ad_of_mem_isCartanSubalgebra, LieModule.trace_toEnd_genWeightSpaceChain_eq_zero, LieModule.maxGenEigenSpace_toEnd_eq_top, LinearEquiv.lieConj_symm, LieAlgebra.rank_eq_natTrailingDegree, instCharPLinearMapSubtypeMemSubringCenterId, IsSemisimple.minpoly_squarefree, LieAlgebra.ad_lie, LieModule.isNilpotent_iff_forall', LieSubmodule.coe_toEnd_pow, LinearMap.isIntegral, LieAlgebra.isNilpotent_range_ad_iff, LieModule.mem_genWeightSpaceOf, LieAlgebra.nilpotent_ad_of_nilpotent_algebra, LieModule.instIsFaithfulEnd, LieModule.coe_lcs_range_toEnd_eq, LieModule.toEnd_module_end, LieAlgebra.mem_zeroRootSubalgebra, instExpCharLinearMapSubtypeMemSubringCenterId, mem_spectrum_iff_isRoot_charpoly, LieAlgebra.commute_ad_of_commute, LieModule.iterate_toEnd_mem_lowerCentralSeries, hasEigenvalue_iff_mem_spectrum, LinearMap.not_hasEigenvalue_zero_tfae, LieDerivation.coe_ad_apply_eq_ad_apply, LieAlgebra.isNilpotent_iff_forall, LieAlgebra.ad_ker_eq_bot_of_hasTrivialRadical, LieAlgebra.isNilpotent_ad_of_isNilpotent, Matrix.minpoly_toLin, LieModule.commute_toEnd_of_mem_center_left, LieAlgebra.ad_ker_eq_self_module_ker, HasUnifEigenvalue.mem_spectrum, LinearMap.IsSymmetric.intCast, LinearMap.instIsSimpleModuleEndOfNontrivial, LieModule.Weight.hasEigenvalueAt, LieModule.rank_le_natTrailingDegree_charpoly_ad, LieSubalgebra.coe_ad, LieModule.toEnd_matrix, LieModule.toEnd_pow_comp_lieHom, LinearMap.trace_lie, Matrix.spectrum_toLin', LieSubalgebra.ad_comp_incl_eq
|
instSemiring 📖 | CompOp | 471 mathmath: LinearMap.det_toContinuousLinearMap, Matrix.toLinAlgEquiv_one, Module.Basis.det_comp_basis, groupHomology.mapCycles₂_comp_assoc, AlgEquiv.moduleEndSelfOp_apply_apply, Rep.trivial_ρ, LinearMap.detAux_def'', LinearMap.toMatrixAlgEquiv'_mul, MeasureTheory.Measure.addHaar_image_continuousLinearMap, LinearMap.exists_monic_and_aeval_eq_zero, groupCohomology.mem_cocycles₂_def, TannakaDuality.FiniteGroup.toRightFDRepComp_in_rightRegular, groupCohomology.d₂₃_hom_apply, smul_def, Polynomial.disjoint_ker_aeval_of_isCoprime, PolynomialModule.smul_def, groupHomology.chainsMap_f_3_comp_chainsIso₃_apply, Rep.resCoindToHom_hom_apply_coe, groupHomology.d₃₂_single, Rep.coindToInd_of_support_subset_orbit, Representation.finsupp_apply, groupHomology.mapCycles₁_comp_apply, FDRep.endRingEquiv_symm_comp_ρ, Representation.Coinvariants.mk_inv_tmul, LinearMap.toMatrixAlgEquiv_comp, LinearMap.det_mulLeft, Representation.asAlgebraHom_single, Representation.freeLift_single_single, Representation.asGroupHom_apply, LinearMap.det_pi, Algebra.lmul_algebraMap, Representation.ofCoinvariantsTprodLeftRegular_mk_tmul_single, LinearMap.det_zero, LinearEquiv.conjAlgEquiv_symm_apply_apply, Representation.linearize_single, isFinitelySemisimple_sub_algebraMap_iff, NonUnitalAlgHom.coe_lmul_eq_mul, groupHomology.mem_cycles₂_iff, Rep.coindToInd_indToCoind, groupCohomology.d₁₂_hom_apply, Rep.to_Module_monoidAlgebra_map_aux, groupHomology.mapCycles₁_comp_assoc, Representation.directSum_apply, LinearMap.toMatrixAlgEquiv_toLinAlgEquiv, IsLocalizedModule.iso_apply_mk, apply_smulCommClass', groupCohomology.d₀₁_hom_apply, Algebra.lmul_injective, Representation.ofMulAction_apply, groupHomology.d₃₂_single_one_thd, Algebra.IsCentral.instEnd, AlgHom.mulLeftRightMatrix.inv_comp, groupCohomology.map_H0Iso_hom_f_apply, Module.endTensorEndAlgHom_apply, Representation.apply_sub_id_partialSum_eq, Representation.asAlgebraHom_def, Orientation.map_eq_neg_iff_det_neg, Representation.Coinvariants.mk_tmul_inv, groupCohomology.mem_cocycles₁_def, RootPairing.Equiv.weightHom_toLinearMap, LinearMap.toMatrixAlgEquiv'_id, LinearEquiv.conjAlgEquiv_apply, Representation.Coinvariants.le_comap_ker, LinearMap.det_baseChange, groupCohomology.mapShortComplexH2_comp_assoc, Module.AEval'.X_smul_of, LinearMap.isUnit_iff_isUnit_det, LocalizedModule.divBy_mul_by, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_apply, groupCohomology.mapCocycles₂_comp_i_apply, ringHomEndFinsupp_apply_apply, Representation.ofMulAction_single, groupHomology.single_one_snd_sub_single_one_fst_mem_boundaries₂, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃_apply, Representation.ofDistribMulAction_apply_apply, LinearMap.toMatrixAlgEquiv_apply, LocalizedModule.lift'_mk, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_apply, groupHomology.d₂₁_single_inv_mul_ρ_add_single, Representation.instIsTrivialSubtypeMemSubgroupSubmoduleInvariantsCompLinearMapIdSubtypeToInvariants, Rep.ActionToRep_obj_ρ, Matrix.toLinAlgEquiv_mul, LinearMap.det_mulRight, Orientation.det_rotation, Representation.Coinvariants.sub_mem_ker, LinearMap.associated_det_of_eq_comp, Orientation.map_eq_iff_det_pos, LinearMap.det_def, Representation.single_smul, Module.AEval'.of_symm_X_smul, QuadraticMap.associated_apply, LinearMap.detAux_def, LinearMap.toMatrixAlgEquiv_id, LinearMap.det_eq_one_of_not_module_finite, Representation.prod_apply_apply, Representation.tprod_apply, MeasureTheory.Measure.map_linearMap_addHaar_eq_smul_addHaar, LinearMap.det_toLpLin, Representation.IntertwiningMap.isIntertwiningMap_of_mem_center, groupHomology.single_one_fst_sub_single_one_snd_mem_boundaries₂, intCast_def, groupCohomology.infNatTrans_app, IsBaseChange.det_endHom, ContinuousLinearMap.toLinearMapRingHom_apply, MeasureTheory.Measure.addHaar_preimage_continuousLinearMap, algebraMap_isUnit_inv_apply_eq_iff', LinearEquiv.det_symm_mul_det, groupHomology.cyclesMap_comp_assoc, Representation.Coinvariants.mk_self_apply, Polynomial.hasseDeriv_comp, Matrix.isRepresentation.toEnd_represents, groupHomology.cyclesMap_comp_cyclesIso₀_hom_apply, Rep.applyAsHom_comm_apply, LieModule.exists_genWeightSpace_le_ker_of_isNoetherian, groupHomology.d₂₁_single_inv_self_ρ_sub_self_inv, Rep.coindFunctorIso_inv_app_hom_toFun_coe, LinearEquiv.symm_conjAlgEquiv, groupCohomology.cocycles₂_map_one_snd, IsSimpleModule.algebraMap_end_bijective_of_isAlgClosed, LinearMap.det_prodMap, TannakaDuality.FiniteGroup.sumSMulInv_apply, Representation.mem_invariants_iff_of_forall_mem_zpowers, Representation.ofQuotient_coe_apply, RootPairing.Hom.coweightHom_injective, Representation.mem_invariants, groupHomology.map_comp_assoc, isLocalizedModule_iff, SpecialLinearGroup.det_eq_one, groupCohomology.cocycles₂_ρ_map_inv_sub_map_inv, LinearMap.pow_eq_aeval_mod_charpoly, LinearMap.tensorProductEnd_apply, Module.AEval'.X_pow_smul_of, rTensorAlgHom_apply_apply, LinearMap.det_eq_det_toMatrix_of_finset, Rep.ofMulDistribMulAction_ρ_apply_apply, IsAzumaya.mulLeftRight_comp_congr, Polynomial.sup_aeval_range_eq_top_of_isCoprime, Rep.RepToAction_map_hom, LinearMap.det_toLin', groupCohomology.cochainsMap_comp_assoc, AlgHom.mulLeftRight_apply, Polynomial.sup_ker_aeval_eq_ker_aeval_mul_of_coprime, FDRep.hom_hom_action_ρ, aeval_apply_of_hasEigenvector, IsAzumaya.bij, Representation.FiniteCyclicGroup.coinvariantsKer_eq_range, Rep.coindToInd_apply, groupHomology.mapCycles₁_comp_i_apply, Complex.det_conjAe, TannakaDuality.FiniteGroup.leftRegular_apply, IsSemisimpleRing.exists_algEquiv_pi_matrix_end_mulOpposite, groupHomology.cyclesIso₀_inv_comp_cyclesMap_apply, Representation.apply_bijective, LinearMap.toMatrixAlgEquiv'_apply, LinearMap.toMatrix'_algebraMap, Representation.linHom_apply, QuadraticMap.associated_toQuadraticMap, DistribMulAction.toModuleEnd_apply, Module.charP_end, Rep.trivial_ρ_apply, LieSubmodule.mapsTo_pow_toEnd_sub_algebraMap, Algebra.PreSubmersivePresentation.jacobian_eq_det_aevalDifferential, Polynomial.det_taylorLinearEquiv_toLinearMap, IsLocalizedModule.fromLocalizedModule_mk, groupCohomology.cocycles₁_map_inv, ringEquivEndFinsupp_apply_apply_apply, isSemisimple_sub_algebraMap_iff, Polynomial.aeval_apply_smul_mem_of_le_comap, Rep.indToCoindAux_mul_fst, Matrix.isRepresentation.toEnd_exists_mem_ideal, Representation.asAlgebraHom_single_one, LinearMap.isUnit_det, Rep.ihom_obj_ρ_apply, Representation.finsupp_single, TannakaDuality.FiniteGroup.equivApp_inv, IsSemisimple.aeval, Algebra.lsmul_injective, groupCohomology.mem_cocycles₂_iff, groupHomology.mapCycles₂_comp_apply, Rep.ofDistribMulAction_ρ_apply_apply, LinearMap.det_eq_zero_iff_ker_ne_bot, Submodule.natAbs_det_equiv, Rep.resCoindHomEquiv_symm_apply, TannakaDuality.FiniteGroup.equivApp_hom, LinearEquiv.isUnit_det', Module.algebraMap_end_eq_smul_id, AlgEquiv.toLinearMapHom_apply_apply, Module.Basis.orientation_comp_linearEquiv_eq_iff_det_pos, groupCohomology.mem_cocycles₁_iff, Rep.coinvariantsShortComplex_f, LinearMap.toMatrix_algebraMap, Representation.norm_comp_self, Module.Basis.orientation_comp_linearEquiv_eq_neg_iff_det_neg, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_apply, Rep.coindVEquiv_apply, Matrix.toLinAlgEquiv'_apply, groupHomology.inhomogeneousChains.d_single, Rep.ActionToRep_map, LinearMap.aeval_eq_aeval_mod_charpoly, Subrepresentation.apply_mem_toSubmodule, LinearMap.det_map, LinearMap.hasEigenvalue_zero_tfae, Representation.coind'_apply_apply, LinearMap.instIsStablyFiniteRingEnd, LinearMap.detAux_def', MeasureTheory.Measure.addHaar_image_linearMap, Module.Invertible.toModuleEnd_bijective, isNilpotent_restrict_maxGenEigenspace_sub_algebraMap, LinearMap.toMatrixAlgEquiv'_toLinAlgEquiv', groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_apply, natCast_def, Representation.asModuleEquiv_symm_map_rho, Representation.freeLift_toLinearMap, Representation.ofModule_asModule_act, IsAzumaya.coe_tensorEquivEnd, LinearMap.eval_charpoly, QuadraticMap.half_moduleEnd_apply_eq_half_smul, LinearMap.toMatrixAlgEquiv_symm, Representation.instIsTrivialSubtypeMemSubgroupCoinvariantsCompLinearMapIdSubtypeToCoinvariants, IsSimpleRing.exists_algEquiv_matrix_end_mulOpposite, LinearMap.det_dualMap, Rep.indToCoindAux_mul_snd, Representation.asAlgebraHom_of, LinearMap.detAux_comp, LinearMap.prodMapAlgHom_apply_apply, det_eq_prod_roots_charpoly_of_splits, LinearMap.det_id, Algebra.toMatrix_lmul', Submodule.det_reflection, Module.Basis.det_comp, LinearMap.det_restrictScalars, MeasureTheory.Measure.addHaar_image_continuousLinearEquiv, RestrictScalars.lsmul_apply_apply, Rep.coe_res_obj_ρ', groupCohomology.cochainsMap_f, inhomogeneousCochains.d_hom_apply, LinearEquiv.conjAlgEquiv_apply_apply, Rep.ρ_mul, groupHomology.d₂₁_single_self_inv_ρ_sub_inv_self, LinearMap.det_eq_sign_charpoly_coeff, exists_isNilpotent_isSemisimple_of_separable_of_dvd_pow, groupHomology.single_ρ_self_add_single_inv_mem_boundaries₁, endVecAlgEquivMatrixEnd_apply_apply, LinearMap.aeval_self_charpoly, Representation.isTrivial_def, Module.algebraMap_end_apply, Ideal.constr_basisSpanSingleton, Rep.FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_toFun, instSMulCommClass', Module.AEval.mem_mapSubmodule_symm_apply, Real.map_linearMap_volume_pi_eq_smul_volume_pi, instIsScalarTower, TannakaDuality.FiniteGroup.sumSMulInv_single_id, apply_smulCommClass, LocalizedModule.lift_mk, Rep.leftRegularHom_hom_single, MeasureTheory.Measure.map_linearMap_addHaar_pi_eq_smul_addHaar, Representation.free_single_single, Representation.IntertwiningMap.isIntertwining', IsSemisimpleModule.exists_end_algEquiv, LinearMap.det_eq_one_of_finrank_eq_zero, Matrix.toLpLinAlgEquiv_apply_apply_ofLp, LocalizedModule.mul_by_divBy, Representation.le_comap_invariants, IsBaseChange.map_id_lsmul_eq_lsmul_algebraMap, Representation.invariants_eq_inter, Matrix.toLinAlgEquiv_apply, AffineMap.linearHom_apply, Representation.subrepresentation_apply, groupCohomology.cocyclesMap_comp_assoc, Module.Basis.det_basis, Representation.norm_self_apply, eigenspace_div, jacobson_density, Polynomial.span_minpoly_eq_annihilator, Rep.indCoindIso_hom_hom_toLinearMap, Representation.smul_tprod_one_asModule, LieModule.isNilpotent_toEnd_sub_algebraMap, Projectivization.smul_def, isNilpotent_tensor_residueField_iff, Polynomial.sup_ker_aeval_le_ker_aeval_mul, LinearMap.det_smul, Rep.RepToAction_obj_ρ, Representation.self_inv_apply, LinearEquiv.isIntertwining_symm_isIntertwining, MeasureTheory.Measure.addHaar_preimage_linearMap, Representation.isTrivial_apply, Ideal.natAbs_det_equiv, Representation.IsIntertwiningMap.isIntertwining, Rep.indResHomEquiv_apply, MeasureTheory.Measure.addHaar_preimage_continuousLinearEquiv, Algebra.toMatrix_lsmul, AlgEquiv.moduleEndSelf_apply_apply, baseChangeHom_apply_apply, groupHomology.single_one_snd_sub_single_one_snd_mem_boundaries₂, Matrix.isRepresentation.toEnd_surjective, Rep.unit_iso_comm, instSMulCommClass, Rep.leftRegularHomEquiv_symm_single, Polynomial.factorial_smul_hasseDeriv, Matrix.toLinAlgEquiv_self, Module.AEval'_def, Module.Finite.toModuleEnd_moduleEnd_surjective, Rep.indCoindIso_inv_hom_toLinearMap, Module.toModuleEnd_apply, LinearMap.det_comp, groupHomology.chainsMap_f_hom, LinearMap.transvection.det, AlgEquiv.moduleEndSelfOp_symm_apply, isNilpotent_restrict_sub_algebraMap, LinearEquiv.det_mul_det_symm, LinearMap.toMatrixAlgEquiv'_symm, LinearMap.IsSymmetric.det_eq_prod_eigenvalues, Representation.IntertwiningMap.isIntertwining_assoc, apply_faithfulSMul, groupCohomology.mapCocycles₁_comp_i_apply, Algebra.norm_apply, Algebra.norm_eq_zero_iff', IsSemisimpleModule.exists_end_algEquiv_pi_matrix_end, Representation.ofModule_asAlgebraHom_apply_apply, LinearMap.det_conj, AlgebraicGeometry.tilde.isUnit_algebraMap_end_basicOpen, Rep.hom_comm_apply, Polynomial.aeval_endomorphism, Matrix.isRepresentation.eq_toEnd_of_represents, Algebra.baseChange_lmul, groupCohomology.cochainsMap_f_hom, Representation.toCoinvariants_mk, AlgEquiv.moduleEndSelf_symm_apply, Rep.quotientToCoinvariantsFunctor_map_hom_toLinearMap, Representation.IsTrivial.out, Matrix.toLinAlgEquiv'_toMatrixAlgEquiv', ker_aeval_ring_hom'_unit_polynomial, Algebra.lmul_isUnit_iff, groupCohomology.mapShortComplexH1_comp_assoc, isStablyFiniteRing_iff_isDedekindFiniteMonoid_moduleEnd, Module.ker_algebraMap_end, Representation.mem_coindV, endVecAlgEquivMatrixEnd_symm_apply_apply, LinearMap.det_zero'', Representation.coind_apply, MeasureTheory.Measure.addHaar_preimage_linearEquiv, Matrix.toLinAlgEquiv'_one, Representation.quotient_apply, lTensorAlgHom_apply_apply, Representation.ind_mk, LinearMap.det_zero', groupHomology.d₂₁_single_one_snd, mem_submonoidCenter_iff, LinearEquiv.coe_inv_det, IsLocalizedModule.fromLocalizedModule'_mk, groupHomology.d₃₂_single_one_snd, FDRep.Iso.conj_ρ, FDRep.of_ρ, det_rotation, Rep.coinvariantsTensorIndHom_mk_tmul_indVMk, instIsStablyFiniteRingEndForallOfFinite, Matrix.toLinAlgEquiv'_symm, Rep.indToCoind_coindToInd, mulSemiringActionToAlgEquiv_conjAct_surjective, IsSemisimpleModule.exists_end_algEquiv_pi_matrix_divisionRing, IsLocalizedModule.map_units, LinearMap.det_ring, LinearMap.coe_det, Representation.linHom.mem_invariants_iff_comm, Rep.indResHomEquiv_symm_apply, ringEquivEndFinsupp_apply_apply_support, Representation.IntertwiningMap.isIntertwining, groupHomology.mapCycles₂_comp_i_apply, PiTensorProduct.mapMonoidHom_apply, LinearMap.det_eq_det_mul_det, AlgHom.toEnd_apply, Representation.asModuleEquiv_map_smul, LinearEquiv.det_coe_symm, groupHomology.d₁₀_single_inv, Representation.ofMulDistribMulAction_apply_apply, Projectivization.generalLinearGroup_smul_def, Rep.res_obj_ρ, LinearMap.det_toMatrix', apply_isScalarTower, LinearMap.toMatrixAlgEquiv_apply', Rep.RepToAction_obj, LinearMap.det_cases, Representation.smul_one_tprod_asModule, natCast_apply, Rep.applyAsHom_apply, Representation.leftRegularMapEquiv_symm_single, groupHomology.d₂₁_single, Algebra.coe_lmul_eq_mul, LinearEquiv.conjAlgEquiv_surjective, LinearMap.not_hasEigenvalue_zero_tfae, Algebra.trace_apply, groupHomology.chainsMap_f_0_comp_chainsIso₀_apply, QuadraticAlgebra.det_toLinearMap_eq_norm, Algebra.FormallyUnramified.comp_sec, groupHomology.single_inv_ρ_self_add_single_mem_boundaries₁, Representation.dual_apply, LinearEquiv.automorphismGroup.toLinearMapMonoidHom_apply, Representation.dualTensorHom_comm, groupHomology.lsingle_comp_chainsMap_f_assoc, LinearMap.toMatrixAlgEquiv_reindexRange, TensorProduct.AlgebraTensorModule.smul_eq_lsmul_rTensor, groupHomology.single_mem_cycles₂_iff, Representation.ind_apply, Representation.isIntertwiningMap_iff, Representation.self_comp_norm, mem_subsemiringCenter_iff, Representation.inv_self_apply, LinearMap.toMatrixAlgEquiv_mul, LinearMap.detAux_id, Representation.apply_eq_of_coe_eq, ringEquivEndFinsupp_symm_apply_apply, LinearMap.det_toMatrix, Rep.coinvariantsTensorIndInv_mk_tmul_indMk, LinearMap.det_toLin, LinearMap.det_eq_one_of_subsingleton, Representation.Equiv.conj_apply_self, groupCohomology.H1InfRes_f, Matrix.Represents.algebraMap, RootPairing.Equiv.coweightHom_toLinearMap, groupHomology.single_mem_cycles₁_iff, groupHomology.d₂₁_single_ρ_add_single_inv_mul, Module.AEval.mem_mapSubmodule_apply, ringHomEndFinsupp_surjective, Representation.asAlgebraHom_mem_of_forall_mem, Matrix.toLpLinAlgEquiv_symm_apply, Representation.mem_linHom_invariants_iff_isIntertwining, Representation.mem_invtSubmodule, exists_isNilpotent_isSemisimple, LinearMap.associated_det_comp_equiv, FDRep.hom_action_ρ, LinearMap.toMatrixAlgEquiv_transpose_apply, eigenspace_aeval_polynomial_degree_1, groupHomology.chainsMap_f_1_comp_chainsIso₁_apply, Algebra.leftMulMatrix_apply, algebraMap_isUnit_inv_apply_eq_iff, RootPairing.Hom.weightHom_injective, groupHomology.H0π_comp_map_apply, Complex.det_conjLIE, Representation.linearize_apply, Matrix.toLinAlgEquiv_toMatrixAlgEquiv, Rep.coinvariantsTensorFreeToFinsupp_mk_tmul_single, TannakaDuality.FiniteGroup.rightRegular_apply, Matrix.toLinAlgEquiv_symm, LinearMap.toMatrixAlgEquiv_transpose_apply', FDRep.endRingEquiv_comp_ρ, groupHomology.mem_cycles₁_iff, Module.instFinitePolynomialAEval', mem_subalgebraCenter_iff, Representation.trivial_apply, groupHomology.single_mem_cycles₂_iff_inv, groupHomology.d₁₀_single, Representation.linearizeTrivial_def, Algebra.lsmul_coe, Representation.self_norm_apply, Representation.IndV.hom_ext_iff, LinearMap.prodMapRingHom_apply, AlgHom.mulLeftRightMatrix.comp_inv, LinearEquiv.coe_det, LinearMap.exists_monic_and_coeff_mem_pow_and_aeval_eq_zero_of_range_le_smul, LinearMap.toMatrixAlgEquiv'_comp, Rep.instIsTrivialVOfCompLinearMapIdρ, Representation.leftRegularMapEquiv_symm_apply_toFun, IsAzumaya.AlgHom.mulLeftRight_bij, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply, groupHomology.chainsMap_f, Rep.quotientToCoinvariantsFunctor_obj_V, groupHomology.chainsMap_f_2_comp_chainsIso₂_apply, groupCohomology.map_comp_assoc, Representation.ofMulAction_def, Rep.coindFunctorIso_hom_app_hom_toFun_hom_toFun
|
smulLeft 📖 | CompOp | 7 mathmath: smulLeft_apply, mem_center_iff, mem_subsemigroupCenter_iff, mem_submonoidCenter_iff, smulLeft_eq, mem_subsemiringCenter_iff, mem_subalgebraCenter_iff
|