Frobenius

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

Statistics

Metric	Count
Definitions `frobenius`, `iterateFrobenius`	2
Theorems `frobenius_def`, `iterateFrobenius_def`, `iterate_map_frobenius`, `map_frobenius`, `map_iterateFrobenius`, `map_iterate_frobenius`, `frobenius_comm`, `iterateFrobenius_comm`, `iterate_map_frobenius`, `map_frobenius`, `map_iterateFrobenius`, `map_iterate_frobenius`, `coe_iterateFrobenius`, `coe_iterateFrobenius_mul`, `frobenius_add`, `frobenius_def`, `frobenius_mul`, `frobenius_natCast`, `frobenius_neg`, `frobenius_one`, `frobenius_sub`, `frobenius_zero`, `iterateFrobenius_add`, `iterateFrobenius_add_apply`, `iterateFrobenius_def`, `iterateFrobenius_eq_pow`, `iterateFrobenius_mul_apply`, `iterateFrobenius_one`, `iterateFrobenius_one_apply`, `iterateFrobenius_zero`, `iterateFrobenius_zero_apply`, `iterate_frobenius`	32
Total	34

LinearMap

Definitions

Name	Category	Theorems
`frobenius` 📖	CompOp	1 math math: `frobenius_def`
`iterateFrobenius` 📖	CompOp	1 math math: `iterateFrobenius_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`frobenius_def` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `frobenius` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `instFunLike` `frobenius` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	—
`iterateFrobenius_def` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `iterateFrobenius` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `instFunLike` `iterateFrobenius` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Nat.instMonoid`	—	—

MonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iterate_map_frobenius` 📖	mathematical	—	`Nat.iterate` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instFunLike` `RingHom` `RingHom.instFunLike` `frobenius`	—	`iterate_map_pow` `instMonoidHomClass`
`map_frobenius` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instFunLike` `RingHom` `RingHom.instFunLike` `frobenius`	—	`map_pow` `instMonoidHomClass`
`map_iterateFrobenius` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instFunLike` `RingHom` `RingHom.instFunLike` `iterateFrobenius`	—	`map_pow` `instMonoidHomClass`
`map_iterate_frobenius` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instFunLike` `Nat.iterate` `RingHom` `RingHom.instFunLike` `frobenius`	—	`Function.Semiconj.iterate_right` `map_frobenius`

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`frobenius_comm` 📖	mathematical	—	`comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `frobenius`	—	`ext` `map_frobenius`
`iterateFrobenius_comm` 📖	mathematical	—	`comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `iterateFrobenius`	—	`ext` `map_iterateFrobenius`
`iterate_map_frobenius` 📖	mathematical	—	`Nat.iterate` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instFunLike` `frobenius`	—	`iterate_map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `instRingHomClass`
`map_frobenius` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instFunLike` `frobenius`	—	`map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `instRingHomClass`
`map_iterateFrobenius` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instFunLike` `iterateFrobenius`	—	`MonoidHom.map_iterateFrobenius`
`map_iterate_frobenius` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instFunLike` `Nat.iterate` `frobenius`	—	`MonoidHom.map_iterate_frobenius`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_iterateFrobenius` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `iterateFrobenius` `Nat.iterate` `frobenius`	—	`pow_iterate`
`coe_iterateFrobenius_mul` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `iterateFrobenius` `Nat.iterate`	—	`iterateFrobenius_mul_apply`
`frobenius_add` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `frobenius` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`RingHom.map_add`
`frobenius_def` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `frobenius` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	—
`frobenius_mul` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `frobenius` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass`
`frobenius_natCast` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `frobenius` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`map_natCast` `RingHom.instRingHomClass`
`frobenius_neg` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `frobenius` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing`	—	`map_neg` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass`
`frobenius_one` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `frobenius` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`one_pow`
`frobenius_sub` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `frobenius` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`map_sub` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass`
`frobenius_zero` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `frobenius` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`RingHom.map_zero`
`iterateFrobenius_add` 📖	mathematical	—	`iterateFrobenius` `RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`RingHom.ext` `iterateFrobenius_add_apply`
`iterateFrobenius_add_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `iterateFrobenius`	—	`add_comm` `pow_add` `pow_mul`
`iterateFrobenius_def` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `iterateFrobenius` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Nat.instMonoid`	—	—
`iterateFrobenius_eq_pow` 📖	mathematical	—	`iterateFrobenius` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Monoid.toNatPow` `RingHom.instMonoid` `frobenius`	—	`RingHom.ext` `iterate_frobenius`
`iterateFrobenius_mul_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `iterateFrobenius` `Nat.iterate`	—	`coe_iterateFrobenius` `Function.iterate_mul`
`iterateFrobenius_one` 📖	mathematical	—	`iterateFrobenius` `frobenius`	—	`RingHom.ext` `iterateFrobenius_one_apply`
`iterateFrobenius_one_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `iterateFrobenius` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`iterateFrobenius_def` `pow_one`
`iterateFrobenius_zero` 📖	mathematical	—	`iterateFrobenius` `RingHom.id` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`RingHom.ext` `iterateFrobenius_zero_apply`
`iterateFrobenius_zero_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `iterateFrobenius`	—	`iterateFrobenius_def` `pow_zero` `pow_one`
`iterate_frobenius` 📖	mathematical	—	`Nat.iterate` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `frobenius` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Nat.instMonoid`	—	`pow_iterate`

---

← Back to Index