trace

📁 Source: MathlibTest/trace.lean

Statistics

Metric	Count
Definitions trace, trace, trace, trace, trace, trace, trace, trace	8
Theorems trace	1
Total	9

Algebra

Definitions

Name	Category	Theorems
trace 📖	CompOp	63 math math: IntermediateField.AdjoinSimple.trace_gen_eq_sum_roots, normalizedTrace_eq_of_finiteDimensional, traceForm_nondegenerate_tfae, trace_eq_of_ringEquiv, trace_eq_of_algEquiv, isIntegral_trace, trace_algebraMap, traceForm_apply, IntermediateField.LinearDisjoint.trace_algebraMap, FiniteField.algebraMap_trace_eq_sum_pow, Submodule.traceDual_top', Module.Basis.trace_traceDual_mul, traceForm_toMatrix, Module.Basis.trace_mul_traceDual, trace_isNilpotent_of_isNilpotent, isNilpotent_trace_of_isNilpotent, differentialIdeal_le_iff, PowerBasis.trace_gen_eq_nextCoeff_minpoly, trace_eq_finrank_mul_minpoly_nextCoeff, normalizedTrace_eq_of_fininteDimensional, trace_eq_trace_adjoin, Subalgebra.LinearDisjoint.trace_algebraMap, trace_self, trace_prod, trace_comp_trace_of_basis, differentialIdeal_le_fractionalIdeal_iff, trace_self_apply, trace_eq_sum_roots, trace_trace, trace_eq_zero_of_not_exists_basis, IntermediateField.AdjoinSimple.trace_gen_eq_zero, trace_localization, trace_eq_matrix_trace, trace_algebraMap_of_basis, trace_quotient_mk, trace_surjective, trace_eq_zero_of_not_isSeparable, normalizedTrace_eq_of_finiteDimensional_apply, trace_complex_apply, normalizedTrace_def, PowerBasis.trace_gen_eq_sum_roots, trace_quotient_eq_trace_localization_quotient, norm_one_add_smul, trace_quotient_eq_of_isDedekindDomain, trace_eq_sum_embeddings, trace_prod_apply, trace_trace_of_basis, traceMatrix_of_basis_mulVec, map_intTraceAux, algebraMap_intTrace, trace_eq_sum_automorphisms, algebraMap_intTrace_fractionRing, normalizedTrace_eq_of_fininteDimensional_apply, trace_apply, coe_trace_int, trace_eq_sum_embeddings_gen, trace_eq_of_equiv_equiv, traceForm_toMatrix_powerBasis, FractionalIdeal.trace_mem_dual_one, trace_comp_trace, intTrace_eq_trace, Submodule.le_traceDual_iff_map_le_one, trace_adjoinSimpleGen

CuspForm

Definitions

Name	Category	Theorems
trace 📖	CompOp	1 math math: coe_trace

Lean.Parser.Tactic

Definitions

Name	Category	Theorems
trace 📖	CompOp	—

LinearMap

Definitions

Name	Category	Theorems
trace 📖	CompOp	53 math math: LieModule.trace_toEnd_eq_zero_of_mem_lcs, trace_mul_cycle, LieModule.trace_toEnd_genWeightSpace, trace_eq_matrix_trace_of_finset, trace_eq_contract_of_basis', trace_smulRight, trace_mul_comm, trace_eq_contract, trace_eq_sum_inner, trace_one, trace_comp_eq_mul_of_commute_of_isNilpotent, InnerProductSpace.trace_rankOne, trace_eq_contract_apply, trace_eq_zero_of_mapsTo_ne, trace_transpose', LieSubmodule.traceForm_eq_zero_of_isTrivial, trace_prodMap, trace_eq_contract', RootPairing.GeckConstruction.trace_toEnd_eq_zero, LieSubmodule.trace_eq_trace_restrict_of_le_idealizer, LieModule.trace_comp_toEnd_genWeightSpace_eq, killingForm_apply_apply, trace_id, Matrix.trace_toLin'_eq, isNilpotent_trace_of_isNilpotent, trace_tensorProduct', trace_transpose, trace_eq_sum_trace_restrict, trace_eq_matrix_trace, trace_conj', Matrix.trace_toLin_eq, LieAlgebra.IsKilling.cartanEquivDual_apply_apply, IsProj.trace, trace_tensorProduct, LieModule.traceForm_apply_apply, IsSymmetric.trace_eq_sum_eigenvalues, LieModule.trace_toEnd_genWeightSpaceChain_eq_zero, trace_eq_contract_of_basis, trace_restrict_eq_of_forall_mem, trace_conj, trace_prodMap', IsSymmetric.re_trace_eq_sum_eigenvalues, trace_comp_comm, trace_eq_sum_trace_restrict', Algebra.trace_apply, trace_comp_cycle, trace_comp_cycle', trace_mul_cycle', trace_comp_comm', trace_baseChange, trace_eq_sum_trace_restrict_of_eq_biSup, trace_map, trace_lie

LinearMap.IsProj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
trace 📖	mathematical	LinearMap.IsProj CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	DFunLike.coe LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Semiring.toModule LinearMap.trace AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Module.finrank Submodule SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module	—	smulCommClass_self RingHomInvPair.ids isCompl eq_conj_prodMap LinearMap.trace_conj' LinearMap.trace_prodMap' LinearMap.trace_id map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass add_zero

Mathlib.Tactic.Translate.Config

Definitions

Name	Category	Theorems
trace 📖	CompOp	—

Matrix

Definitions

Name	Category	Theorems
trace 📖	CompOp	89 math math: trace_mul_conjTranspose_self_eq_zero_iff, trace_units_conj, trace_blockDiagonal', trace_single_eq_same, RootPairing.GeckConstruction.trace_h_eq_zero, trace_kronecker, trace_transpose, sum_hadamard_eq, ZMod.trace_pow_card, trace_eq_neg_charpoly_coeff, LinearMap.trace_eq_matrix_trace_of_finset, derivative_det_one_add_X_smul, trace_multiset_sum, AddMonoidHom.map_trace, trace_mul_comm, ext_iff_trace_mul_right, det_one_add_smul, trace_fin_zero, PosSemidef.trace_eq_zero_iff, star_vec_dotProduct_vec, vec_dotProduct_vec, trace_diagonal, IsHermitian.trace_eq_sum_eigenvalues, trace_eq_zero_of_isEmpty, Continuous.matrix_trace, trace_fin_two, ext_iff_trace_mul_left, trace_sum, trace_replicateCol_mul_replicateRow, det_one_add_X_smul, trace_eq_sum_roots_charpoly, discr_of_card_eq_two, coeff_charpolyRev_eq_neg_trace, traceLinearMap_apply, trace_single_eq_of_ne, trace_eq_sum_roots_charpoly_of_splits, trace_conjTranspose_mul_self_eq_zero_iff, trace_eq_neg_charpoly_nextCoeff, trace_conjTranspose, charpoly_fin_two, trace_fin_one_of, sub_scalar_sq_eq_disc, disc_fin_two, FiniteField.trace_pow_card, trace_single_mul, PosDef.trace_pos, trace_toLin'_eq, trace_list_sum, trace_fin_three, trace_add, Algebra.trace_eq_matrix_trace, traceAddMonoidHom_apply, trace_fin_one, LieAlgebra.matrix_trace_commutator_zero, dotProduct_vecMul_hadamard, LinearMap.trace_eq_matrix_trace, trace_submatrix_succ, trace_vecMulVec, coeff_det_one_add_X_smul_one, trace_toLin_eq, trace_mul_single, trace_transpose_mul, trace_one, trace_kroneckerTMul, trace_fin_three_of, trace_permutation, trace_kroneckerMapBilinear, trace_smul, isNilpotent_trace_of_isNilpotent, disc_of_card_eq_two, trace_blockDiagonal, trace_sub, PosSemidef.trace_nonneg, trace_surjective, trace_zero, trace_mul_cycle, trace_units_conj', trace_map, trace_neg, trace_mul_cycle', derivative_det_one_add_X_smul_aux, sub_scalar_sq_eq_discr, SimpleGraph.trace_adjMatrix, trace_conj', LinearMap.traceAux_def, trace_fin_two_of, trace_conj, charpoly_of_card_eq_two, discr_fin_two

ModularForm

Definitions

Name	Category	Theorems
trace 📖	CompOp	1 math math: coe_trace

SlashInvariantForm

Definitions

Name	Category	Theorems
trace 📖	CompOp	1 math math: coe_trace

---

← Back to Index