FiniteField

📁 Source: Mathlib/LinearAlgebra/Matrix/Charpoly/FiniteField.lean

Statistics

Metric	Count
Definitions	0
Theorems charpoly_pow_card, trace_pow_card, charpoly_pow_card, trace_pow_card	4
Total	4

FiniteField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
trace_pow_card 📖	mathematical	—	Matrix.trace NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Matrix Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Fintype.card	—	isEmpty_or_nonempty Finset.sum_congr Finset.univ_eq_empty zero_pow Nontrivial.to_nonempty IsLocalRing.toNontrivial Field.instIsLocalRing Matrix.trace_eq_neg_charpoly_coeff Matrix.charpoly_pow_card pow_card

FiniteField.Matrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
charpoly_pow_card 📖	mathematical	—	Matrix.charpoly EuclideanDomain.toCommRing Field.toEuclideanDomain Matrix Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Fintype.card	—	isEmpty_or_nonempty CharP.exists FiniteField.card Function.Injective.iterate Polynomial.instExpChar expChar_prime isReduced_of_noZeroDivisors Polynomial.instNoZeroDivisors IsDomain.to_noZeroDivisors instIsDomain iterate_frobenius FiniteField.expand_card AlgHom.map_det Matrix.coe_detMonoidHom MonoidHom.map_pow AlgEquiv.injective map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass Matrix.matPolyEquiv_charmatrix sub_pow_char_pow_of_commute Polynomial.instCharP Matrix.charP Polynomial.commute_X Polynomial.C_pow AlgHom.algHomClass matPolyEquiv_eq_X_pow_sub_C Matrix.subsingleton_of_empty_right

ZMod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
charpoly_pow_card 📖	mathematical	—	Matrix.charpoly ZMod commRing Matrix Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField	—	NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' FiniteField.Matrix.charpoly_pow_card card
trace_pow_card 📖	mathematical	—	Matrix.trace ZMod NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing Matrix Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField	—	NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' FiniteField.trace_pow_card card

---

← Back to Index