Trace

📁 Source: Mathlib/FieldTheory/Finite/Trace.lean

Statistics

Metric	Count
Definitions	0
Theorems algebraMap_norm_eq_pow_sum, algebraMap_norm_eq_prod_pow, algebraMap_trace_eq_sum_pow, trace_to_zmod_nondegenerate	4
Total	4

FiniteField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_norm_eq_pow_sum 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Ring.toSemiring DivisionRing.toRing Field.toDivisionRing CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain MonoidHom.instFunLike Algebra.norm Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Finset.sum Nat.instAddCommMonoid Finset.range Module.finrank NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Nat.instMonoid Nat.card	—	algebraMap_norm_eq_prod_pow Finset.prod_pow_eq_pow_sum
algebraMap_norm_eq_prod_pow 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Ring.toSemiring DivisionRing.toRing Field.toDivisionRing CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain MonoidHom.instFunLike Algebra.norm Finset.prod CommRing.toCommMonoid Finset.range Module.finrank NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Nat.instMonoid Nat.card	—	Finite.of_injective FaithfulSMul.algebraMap_injective Module.Free.instFaithfulSMulOfNontrivial Module.Free.of_divisionRing IsLocalRing.toNontrivial Field.instIsLocalRing Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective Module.IsNoetherian.finite isNoetherian_of_isNoetherianRing_of_finite PrincipalIdealRing.isNoetherianRing EuclideanDomain.to_principal_ideal_domain isNoetherian_of_finite Module.Projective.of_free Algebra.norm_eq_prod_automorphisms GaloisField.instIsGaloisOfFinite Finset.prod_range Fintype.prod_bijective Algebra.IsAlgebraic.of_finite bijective_frobeniusAlgEquivOfAlgebraic_pow AlgEquiv.coe_pow coe_frobeniusAlgEquivOfAlgebraic_iterate Fintype.card_eq_nat_card
algebraMap_trace_eq_sum_pow 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap LinearMap CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Semiring.toModule LinearMap.instFunLike Algebra.trace Finset.sum Finset.range Module.finrank Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Nat.instMonoid Nat.card	—	Finite.of_injective FaithfulSMul.algebraMap_injective Module.Free.instFaithfulSMulOfNontrivial Module.Free.of_divisionRing IsLocalRing.toNontrivial Field.instIsLocalRing Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective Module.IsNoetherian.finite isNoetherian_of_isNoetherianRing_of_finite PrincipalIdealRing.isNoetherianRing EuclideanDomain.to_principal_ideal_domain isNoetherian_of_finite Module.Projective.of_free trace_eq_sum_automorphisms GaloisField.instIsGaloisOfFinite Finset.sum_range Fintype.sum_bijective Algebra.IsAlgebraic.of_finite bijective_frobeniusAlgEquivOfAlgebraic_pow AlgEquiv.coe_pow coe_frobeniusAlgEquivOfAlgebraic_iterate Fintype.card_eq_nat_card
trace_to_zmod_nondegenerate 📖	—	—	—	—	CharP.char_is_prime IsDomain.to_noZeroDivisors instIsDomain IsLocalRing.toNontrivial Field.instIsLocalRing ringChar.charP traceForm_nondegenerate Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective Module.IsNoetherian.finite isNoetherian_of_isNoetherianRing_of_finite PrincipalIdealRing.isNoetherianRing EuclideanDomain.to_principal_ideal_domain isNoetherian_of_finite Module.Projective.of_free Module.Free.of_divisionRing Algebra.IsAlgebraic.isSeparable_of_perfectField Algebra.IsSeparable.isAlgebraic ZMod.nontrivial Nat.Prime.one_lt' IsGalois.to_isSeparable GaloisField.instIsGaloisOfFinite PerfectField.ofFinite Finite.of_fintype NeZero.of_gt' Nat.instCanonicallyOrderedAdd

---

← Back to Index