Reduced

📁 Source: Mathlib/Algebra/CharP/Reduced.lean

Statistics

Metric	Count
Definitions	0
Theorems pow_prime_pow_mul_eq_one_iff, frobenius_inj, isSquare_of_charTwo', iterateFrobenius_inj	4
Total	4

ExpChar

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pow_prime_pow_mul_eq_one_iff 📖	mathematical	—	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Nat.instMonoid AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	pow_mul' map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
frobenius_inj 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike frobenius	—	iterateFrobenius_one
isSquare_of_charTwo' 📖	mathematical	—	IsSquare Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	nonempty_fintype pow_two Function.Bijective.surjective expChar_prime Nat.fact_prime_two Fintype.bijective_iff_injective_and_card
iterateFrobenius_inj 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike iterateFrobenius	—	sub_eq_zero IsReduced.eq_zero

---

← Back to Index