Mathlib.Algebra.CharP.Frobenius

frobenius_def theorem

: frobenius R p x = x ^ p

Full source

lemma frobenius_def : frobenius R p x = x ^ p := rfl

Frobenius Endomorphism Formula: $\text{Frob}_p(x) = x^p$

Informal description

For a commutative semiring $R$ with exponential characteristic $p$, the Frobenius endomorphism $\text{Frob}_p$ evaluated at an element $x \in R$ is equal to $x$ raised to the power $p$, i.e., \[ \text{Frob}_p(x) = x^p. \]

iterateFrobenius_def theorem

: iterateFrobenius R p n x = x ^ p ^ n

Full source

lemma iterateFrobenius_def : iterateFrobenius R p n x = x ^ p ^ n := rfl

Iterated Frobenius Endomorphism Formula: $\text{Frob}_{p^n}(x) = x^{p^n}$

Informal description

For a commutative semiring $R$ with exponential characteristic $p$ and any natural number $n$, the $n$-th iterate of the Frobenius endomorphism evaluated at $x \in R$ is equal to $x$ raised to the power $p^n$, i.e., \[ \text{Frob}_{p^n}(x) = x^{p^n}. \]

iterate_frobenius theorem

: (frobenius R p)^[n] x = x ^ p ^ n

Full source

lemma iterate_frobenius : (frobenius R p)^[n] x = x ^ p ^ n := congr_fun (pow_iterate p n) x

Iterated Frobenius Formula: $\text{Frob}_p^n(x) = x^{p^n}$

Informal description

For a commutative semiring $R$ with exponential characteristic $p$ and any natural number $n$, the $n$-th iterate of the Frobenius endomorphism $\text{Frob}_p$ applied to an element $x \in R$ satisfies: \[ \text{Frob}_p^n(x) = x^{p^n}. \]

iterateFrobenius_eq_pow theorem

: iterateFrobenius R p n = frobenius R p ^ n

Full source

lemma iterateFrobenius_eq_pow : iterateFrobenius R p n = frobenius R p ^ n := by
  ext; simp [iterateFrobenius_def, iterate_frobenius]

Iterated Frobenius as Power of Frobenius: $\text{Frob}_{p^n} = (\text{Frob}_p)^n$

Informal description

For a commutative semiring $R$ with exponential characteristic $p$ and any natural number $n$, the $n$-th iterate of the Frobenius endomorphism $\text{Frob}_{p^n}$ is equal to the $n$-th power of the Frobenius endomorphism $\text{Frob}_p$, i.e., \[ \text{Frob}_{p^n} = (\text{Frob}_p)^n. \]

coe_iterateFrobenius theorem

: iterateFrobenius R p n = (frobenius R p)^[n]

Full source

lemma coe_iterateFrobenius : iterateFrobenius R p n = (frobenius R p)^[n] :=
  (pow_iterate p n).symm

Iterated Frobenius as Composition of Frobenius Endomorphisms

Informal description

For a commutative semiring $R$ with exponential characteristic $p$, the $n$-th iterate of the Frobenius endomorphism $\text{Frob}_p : R \to R$ (defined by $x \mapsto x^p$) is equal to the ring homomorphism $\text{Frob}_{p^n} : R \to R$ (defined by $x \mapsto x^{p^n}$). In other words, $\text{Frob}_{p^n} = (\text{Frob}_p)^{\circ n}$ where $(\text{Frob}_p)^{\circ n}$ denotes the $n$-fold composition of $\text{Frob}_p$ with itself.

iterateFrobenius_one_apply theorem

: iterateFrobenius R p 1 x = x ^ p

Full source

lemma iterateFrobenius_one_apply : iterateFrobenius R p 1 x = x ^ p := by
  rw [iterateFrobenius_def, pow_one]

First Iterate of Frobenius Endomorphism: $\text{Frob}_p(x) = x^p$

Informal description

For a commutative semiring $R$ with exponential characteristic $p$, the first iterate of the Frobenius endomorphism evaluated at an element $x \in R$ is equal to $x$ raised to the power $p$, i.e., \[ \text{Frob}_p(x) = x^p. \]

iterateFrobenius_one theorem

: iterateFrobenius R p 1 = frobenius R p

Full source

@[simp]
lemma iterateFrobenius_one : iterateFrobenius R p 1 = frobenius R p :=
  RingHom.ext (iterateFrobenius_one_apply R p)

First Iterate of Frobenius Endomorphism Equals Frobenius Endomorphism

Informal description

For a commutative semiring $R$ with exponential characteristic $p$, the first iterate of the Frobenius endomorphism is equal to the Frobenius endomorphism itself, i.e., \[ \text{Frob}_{p^1} = \text{Frob}_p. \]

iterateFrobenius_zero_apply theorem

: iterateFrobenius R p 0 x = x

Full source

lemma iterateFrobenius_zero_apply : iterateFrobenius R p 0 x = x := by
  rw [iterateFrobenius_def, pow_zero, pow_one]

Identity Action of Zeroth Frobenius Iterate: $\text{Frob}_{p^0}(x) = x$

Informal description

For any commutative semiring $R$ with exponential characteristic $p$ and any element $x \in R$, the zeroth iterate of the Frobenius endomorphism acts as the identity function, i.e., \[ \text{Frob}_{p^0}(x) = x. \]

iterateFrobenius_zero theorem

: iterateFrobenius R p 0 = RingHom.id R

Full source

@[simp]
lemma iterateFrobenius_zero : iterateFrobenius R p 0 = RingHom.id R :=
  RingHom.ext (iterateFrobenius_zero_apply R p)

Zeroth Frobenius Iterate is Identity: $\text{Frob}_{p^0} = \text{id}_R$

Informal description

For any commutative semiring $R$ with exponential characteristic $p$, the zeroth iterate of the Frobenius endomorphism is equal to the identity ring homomorphism on $R$, i.e., \[ \text{Frob}_{p^0} = \text{id}_R. \]

iterateFrobenius_add_apply theorem

: iterateFrobenius R p (m + n) x = iterateFrobenius R p m (iterateFrobenius R p n x)

Full source

lemma iterateFrobenius_add_apply :
    iterateFrobenius R p (m + n) x = iterateFrobenius R p m (iterateFrobenius R p n x) := by
  simp_rw [iterateFrobenius_def, add_comm m n, pow_add, pow_mul]

Additivity of Iterated Frobenius Homomorphism: $\text{Frob}_{p^{m+n}}(x) = \text{Frob}_{p^m}(\text{Frob}_{p^n}(x))$

Informal description

Let $R$ be a commutative semiring with exponential characteristic $p$. For any natural numbers $m, n$ and any element $x \in R$, the iterated Frobenius homomorphism satisfies \[ \text{Frob}_{p^{m+n}}(x) = \text{Frob}_{p^m}(\text{Frob}_{p^n}(x)). \]

iterateFrobenius_add theorem

: iterateFrobenius R p (m + n) = (iterateFrobenius R p m).comp (iterateFrobenius R p n)

Full source

lemma iterateFrobenius_add :
    iterateFrobenius R p (m + n) = (iterateFrobenius R p m).comp (iterateFrobenius R p n) :=
  RingHom.ext (iterateFrobenius_add_apply R p m n)

Additivity of Iterated Frobenius Homomorphism Composition: $\text{Frob}_{p^{m+n}} = \text{Frob}_{p^m} \circ \text{Frob}_{p^n}$

Informal description

Let $R$ be a commutative semiring with exponential characteristic $p$. For any natural numbers $m$ and $n$, the iterated Frobenius homomorphism satisfies \[ \text{Frob}_{p^{m+n}} = \text{Frob}_{p^m} \circ \text{Frob}_{p^n}, \] where $\circ$ denotes the composition of ring homomorphisms.

iterateFrobenius_mul_apply theorem

: iterateFrobenius R p (m * n) x = (iterateFrobenius R p m)^[n] x

Full source

lemma iterateFrobenius_mul_apply :
    iterateFrobenius R p (m * n) x = (iterateFrobenius R p m)^[n] x := by
  simp_rw [coe_iterateFrobenius, Function.iterate_mul]

Multiplicative Property of Iterated Frobenius: $\text{Frob}_{p^{m \cdot n}}(x) = (\text{Frob}_{p^m})^{[n]}(x)$

Informal description

Let $R$ be a commutative semiring with exponential characteristic $p$. For any natural numbers $m, n$ and any element $x \in R$, the iterated Frobenius homomorphism satisfies \[ \text{Frob}_{p^{m \cdot n}}(x) = (\text{Frob}_{p^m})^{[n]}(x), \] where $(\text{Frob}_{p^m})^{[n]}$ denotes the $n$-fold composition of $\text{Frob}_{p^m}$ with itself.

coe_iterateFrobenius_mul theorem

: iterateFrobenius R p (m * n) = (iterateFrobenius R p m)^[n]

Full source

lemma coe_iterateFrobenius_mul : iterateFrobenius R p (m * n) = (iterateFrobenius R p m)^[n] :=
  funext (iterateFrobenius_mul_apply R p m n)

Multiplicative Property of Iterated Frobenius Homomorphism: $\text{Frob}_{p^{m \cdot n}} = (\text{Frob}_{p^m})^n$

Informal description

Let $R$ be a commutative semiring with exponential characteristic $p$. For any natural numbers $m$ and $n$, the iterated Frobenius homomorphism satisfies \[ \text{Frob}_{p^{m \cdot n}} = (\text{Frob}_{p^m})^n, \] where $(\text{Frob}_{p^m})^n$ denotes the $n$-fold composition of $\text{Frob}_{p^m}$ with itself.

frobenius_mul theorem

: frobenius R p (x * y) = frobenius R p x * frobenius R p y

Full source

lemma frobenius_mul : frobenius R p (x * y) = frobenius R p x * frobenius R p y :=
  map_mul (frobenius R p) x y

Multiplicativity of the Frobenius Endomorphism: $\text{Frob}_p(x \cdot y) = \text{Frob}_p(x) \cdot \text{Frob}_p(y)$

Informal description

Let $R$ be a commutative semiring with exponential characteristic $p$. The Frobenius endomorphism $\text{Frob}_p \colon R \to R$ satisfies $\text{Frob}_p(x \cdot y) = \text{Frob}_p(x) \cdot \text{Frob}_p(y)$ for all $x, y \in R$.

frobenius_one theorem

: frobenius R p 1 = 1

Full source

lemma frobenius_one : frobenius R p 1 = 1 := one_pow _

Frobenius Endomorphism Preserves Multiplicative Identity

Informal description

For a commutative semiring $R$ with exponential characteristic $p$, the Frobenius endomorphism $\text{Frob}_p$ satisfies $\text{Frob}_p(1) = 1$.

MonoidHom.map_frobenius theorem

: f (frobenius R p x) = frobenius S p (f x)

Full source

lemma MonoidHom.map_frobenius : f (frobenius R p x) = frobenius S p (f x) := map_pow f x p

Frobenius Endomorphism Commutes with Monoid Homomorphisms

Informal description

Let $R$ and $S$ be commutative semirings with exponential characteristic $p$, and let $f \colon R \to S$ be a monoid homomorphism. Then for any $x \in R$, the image of the Frobenius endomorphism $\text{Frob}_p(x) = x^p$ under $f$ is equal to the Frobenius endomorphism applied to $f(x)$, i.e., \[ f(x^p) = (f(x))^p. \]

RingHom.map_frobenius theorem

: g (frobenius R p x) = frobenius S p (g x)

Full source

lemma RingHom.map_frobenius : g (frobenius R p x) = frobenius S p (g x) := map_pow g x p

Ring Homomorphism Commutes with Frobenius Endomorphism

Informal description

Let $R$ and $S$ be commutative semirings with exponential characteristic $p$, and let $g \colon R \to S$ be a ring homomorphism. Then for any element $x \in R$, the homomorphism $g$ commutes with the Frobenius endomorphism, i.e., \[ g(x^p) = (g(x))^p. \]

MonoidHom.map_iterate_frobenius theorem

(n : ℕ) : f ((frobenius R p)^[n] x) = (frobenius S p)^[n] (f x)

Full source

lemma MonoidHom.map_iterate_frobenius (n : ℕ) :
    f ((frobenius R p)^[n] x) = (frobenius S p)^[n] (f x) :=
  Function.Semiconj.iterate_right (f.map_frobenius p) n x

Monoid Homomorphism Commutes with Iterated Frobenius Endomorphism

Informal description

Let $R$ and $S$ be commutative semirings with exponential characteristic $p$, and let $f \colon R \to S$ be a monoid homomorphism. Then for any natural number $n$ and any element $x \in R$, the homomorphism $f$ commutes with the $n$-th iterate of the Frobenius endomorphism, i.e., \[ f(x^{p^n}) = (f(x))^{p^n}. \]

MonoidHom.map_iterateFrobenius theorem

(n : ℕ) : f (iterateFrobenius R p n x) = iterateFrobenius S p n (f x)

Full source

lemma MonoidHom.map_iterateFrobenius (n : ℕ) :
    f (iterateFrobenius R p n x) = iterateFrobenius S p n (f x) := by
  simp [iterateFrobenius_def]

Monoid Homomorphism Commutes with Iterated Frobenius

Informal description

Let $R$ and $S$ be commutative semirings with exponential characteristic $p$, and let $f \colon R \to S$ be a monoid homomorphism. Then for any natural number $n$ and any element $x \in R$, the homomorphism $f$ commutes with the $n$-th iterate of the Frobenius endomorphism, i.e., \[ f(\text{Frob}_{p^n}(x)) = \text{Frob}_{p^n}(f(x)), \] where $\text{Frob}_{p^n}(x) = x^{p^n}$ denotes the $n$-th iterate of the Frobenius endomorphism.

RingHom.map_iterate_frobenius theorem

(n : ℕ) : g ((frobenius R p)^[n] x) = (frobenius S p)^[n] (g x)

Full source

lemma RingHom.map_iterate_frobenius (n : ℕ) :
    g ((frobenius R p)^[n] x) = (frobenius S p)^[n] (g x) :=
  g.toMonoidHom.map_iterate_frobenius p x n

Ring homomorphism commutes with iterated Frobenius: $g(x^{p^n}) = g(x)^{p^n}$

Informal description

Let $R$ and $S$ be commutative semirings with exponential characteristic $p$, and let $g \colon R \to S$ be a ring homomorphism. Then for any natural number $n$ and any element $x \in R$, the homomorphism $g$ commutes with the $n$-th iterate of the Frobenius endomorphism, i.e., \[ g(x^{p^n}) = (g(x))^{p^n}. \]

RingHom.map_iterateFrobenius theorem

(n : ℕ) : g (iterateFrobenius R p n x) = iterateFrobenius S p n (g x)

Full source

lemma RingHom.map_iterateFrobenius (n : ℕ) :
    g (iterateFrobenius R p n x) = iterateFrobenius S p n (g x) :=
  g.toMonoidHom.map_iterateFrobenius p x n

Ring Homomorphism Commutes with Iterated Frobenius Endomorphism

Informal description

Let $R$ and $S$ be commutative semirings with exponential characteristic $p$, and let $g \colon R \to S$ be a ring homomorphism. Then for any natural number $n$ and any element $x \in R$, the homomorphism $g$ commutes with the $n$-th iterate of the Frobenius endomorphism, i.e., \[ g(x^{p^n}) = (g(x))^{p^n}, \] where $x^{p^n}$ denotes the $n$-th iterate of the Frobenius endomorphism.

MonoidHom.iterate_map_frobenius theorem

(f : R →* R) (p : ℕ) [ExpChar R p] (n : ℕ) : f^[n] (frobenius R p x) = frobenius R p (f^[n] x)

Full source

lemma MonoidHom.iterate_map_frobenius (f : R →* R) (p : ℕ) [ExpChar R p] (n : ℕ) :
    f^[n] (frobenius R p x) = frobenius R p (f^[n] x) :=
  iterate_map_pow f _ _ _

Iterated Monoid Homomorphism Commutes with Frobenius Endomorphism

Informal description

Let $R$ be a commutative semiring with exponential characteristic $p$, and let $f \colon R \to R$ be a monoid homomorphism. For any natural number $n$ and any element $x \in R$, the $n$-th iterate of $f$ applied to the Frobenius endomorphism of $x$ equals the Frobenius endomorphism applied to the $n$-th iterate of $f$ at $x$, i.e., $$ f^{[n]}(\text{Frob}_p(x)) = \text{Frob}_p(f^{[n]}(x)). $$

RingHom.iterate_map_frobenius theorem

(f : R →+* R) (p : ℕ) [ExpChar R p] (n : ℕ) : f^[n] (frobenius R p x) = frobenius R p (f^[n] x)

Full source

lemma RingHom.iterate_map_frobenius (f : R →+* R) (p : ℕ) [ExpChar R p] (n : ℕ) :
    f^[n] (frobenius R p x) = frobenius R p (f^[n] x) := iterate_map_pow f _ _ _

Iterated Ring Homomorphism Commutes with Frobenius: $f^{[n]}(x^p) = (f^{[n]}(x))^p$

Informal description

Let $R$ be a commutative semiring with exponential characteristic $p$, and let $f : R \to R$ be a ring homomorphism. For any natural number $n$ and any element $x \in R$, the $n$-th iterate of $f$ applied to the Frobenius endomorphism $\text{Frob}_p(x) = x^p$ equals the Frobenius endomorphism applied to the $n$-th iterate of $f$ at $x$, i.e., $$ f^{[n]}(x^p) = (f^{[n]}(x))^p. $$

RingHom.frobenius_comm theorem

: g.comp (frobenius R p) = (frobenius S p).comp g

Full source

/-- The Frobenius endomorphism commutes with any ring homomorphism. -/
lemma RingHom.frobenius_comm : g.comp (frobenius R p) = (frobenius S p).comp g :=
  ext <| map_frobenius g p

Commutativity of Ring Homomorphisms with Frobenius Endomorphism

Informal description

Let $R$ and $S$ be commutative semirings with exponential characteristic $p$, and let $g \colon R \to S$ be a ring homomorphism. Then the composition of $g$ with the Frobenius endomorphism on $R$ equals the composition of the Frobenius endomorphism on $S$ with $g$, i.e., \[ g \circ \text{Frob}_p = \text{Frob}_p \circ g. \]

RingHom.iterateFrobenius_comm theorem

(n : ℕ) : g.comp (iterateFrobenius R p n) = (iterateFrobenius S p n).comp g

Full source

/-- The iterated Frobenius endomorphism commutes with any ring homomorphism. -/
lemma RingHom.iterateFrobenius_comm (n : ℕ) :
    g.comp (iterateFrobenius R p n) = (iterateFrobenius S p n).comp g :=
  ext fun x ↦ map_iterateFrobenius g p x n

Commutativity of Ring Homomorphism with Iterated Frobenius Endomorphism

Informal description

Let $R$ and $S$ be commutative semirings with exponential characteristic $p$, and let $g \colon R \to S$ be a ring homomorphism. Then for any natural number $n$, the following diagram commutes: \[ \begin{CD} R @>{g}>> S \\ @V{\text{Frob}_{p^n}}VV @VV{\text{Frob}_{p^n}}V \\ R @>>{g}> S \end{CD} \] where $\text{Frob}_{p^n}$ denotes the $n$-th iterate of the Frobenius endomorphism, i.e., $\text{Frob}_{p^n}(x) = x^{p^n}$ for all $x \in R$ or $x \in S$.

LinearMap.frobenius definition

[Algebra R S] : S →ₛₗ[frobenius R p] S

Full source

/-- The frobenius map of an algebra as a frobenius-semilinear map. -/
nonrec def LinearMap.frobenius [Algebra R S] : S →ₛₗ[frobenius R p] S where
  __ := frobenius S p
  map_smul' r s := show frobenius S p _ = _ by
    simp_rw [Algebra.smul_def, map_mul, ← (algebraMap R S).map_frobenius]; rfl

Frobenius semilinear map

Informal description

Given a commutative semiring $R$ with exponential characteristic $p$ and an $R$-algebra $S$, the Frobenius map $\text{Frob}_p \colon S \to S$ is a semilinear map with respect to the Frobenius endomorphism $\text{Frob}_p \colon R \to R$. Explicitly, for any $x \in S$, the map sends $x$ to $x^p$ and satisfies the semilinearity condition $\text{Frob}_p(r \cdot x) = \text{Frob}_p(r) \cdot \text{Frob}_p(x)$ for all $r \in R$ and $x \in S$.

LinearMap.iterateFrobenius definition

[Algebra R S] : S →ₛₗ[iterateFrobenius R p n] S

Full source

/-- The iterated frobenius map of an algebra as a iterated-frobenius-semilinear map. -/
nonrec def LinearMap.iterateFrobenius [Algebra R S] : S →ₛₗ[iterateFrobenius R p n] S where
  __ := iterateFrobenius S p n
  map_smul' f s := show iterateFrobenius S p n _ = _ by
    simp_rw [iterateFrobenius_def, Algebra.smul_def, mul_pow, ← map_pow]; rfl

Iterated Frobenius semilinear map

Informal description

Given a commutative semiring $R$ with exponential characteristic $p$ and an $R$-algebra $S$, the iterated Frobenius map $\text{Frob}_{p^n} \colon S \to S$ is a semilinear map with respect to the iterated Frobenius endomorphism $\text{Frob}_{p^n} \colon R \to R$. Explicitly, for any $x \in S$, the map sends $x$ to $x^{p^n}$ and satisfies the semilinearity condition $\text{Frob}_{p^n}(r \cdot x) = \text{Frob}_{p^n}(r) \cdot \text{Frob}_{p^n}(x)$ for all $r \in R$ and $x \in S$.

LinearMap.frobenius_def theorem

[Algebra R S] (x : S) : frobenius R S p x = x ^ p

Full source

theorem LinearMap.frobenius_def [Algebra R S] (x : S) : frobenius R S p x = x ^ p := rfl

Frobenius Map Formula: $\text{Frob}_p(x) = x^p$

Informal description

Let $R$ be a commutative semiring with exponential characteristic $p$, and let $S$ be an $R$-algebra. For any element $x \in S$, the Frobenius map $\text{Frob}_p$ satisfies $\text{Frob}_p(x) = x^p$.

LinearMap.iterateFrobenius_def theorem

[Algebra R S] (n : ℕ) (x : S) : iterateFrobenius R S p n x = x ^ p ^ n

Full source

theorem LinearMap.iterateFrobenius_def [Algebra R S] (n : ℕ) (x : S) :
    iterateFrobenius R S p n x = x ^ p ^ n := rfl

Iterated Frobenius Map Formula: $\text{Frob}_{p^n}(x) = x^{p^n}$

Informal description

Let $R$ be a commutative semiring with exponential characteristic $p$, and let $S$ be an $R$-algebra. For any natural number $n$ and any element $x \in S$, the iterated Frobenius map $\text{Frob}_{p^n}$ satisfies $\text{Frob}_{p^n}(x) = x^{p^n}$.

frobenius_zero theorem

: frobenius R p 0 = 0

Full source

theorem frobenius_zero : frobenius R p 0 = 0 :=
  (frobenius R p).map_zero

Frobenius Endomorphism Preserves Zero

Informal description

The Frobenius endomorphism $\text{Frob}_p$ on a commutative semiring $R$ of characteristic exponent $p$ maps the zero element to itself, i.e., $\text{Frob}_p(0) = 0$.

frobenius_add theorem

: frobenius R p (x + y) = frobenius R p x + frobenius R p y

Full source

theorem frobenius_add : frobenius R p (x + y) = frobenius R p x + frobenius R p y :=
  (frobenius R p).map_add x y

Additivity of the Frobenius Endomorphism: $\text{Frob}_p(x + y) = \text{Frob}_p(x) + \text{Frob}_p(y)$

Informal description

For any commutative semiring $R$ with exponential characteristic $p$, the Frobenius endomorphism $\text{Frob}_p : R \to R$ satisfies $\text{Frob}_p(x + y) = \text{Frob}_p(x) + \text{Frob}_p(y)$ for all $x, y \in R$.

frobenius_natCast theorem

(n : ℕ) : frobenius R p n = n

Full source

theorem frobenius_natCast (n : ℕ) : frobenius R p n = n :=
  map_natCast (frobenius R p) n

Frobenius Endomorphism Fixes Natural Numbers in Characteristic $p$

Informal description

For any natural number $n$ and any commutative semiring $R$ with exponential characteristic $p$, the Frobenius endomorphism $\text{Frob}_p$ satisfies $\text{Frob}_p(n) = n$, where $n$ is interpreted as an element of $R$ via the natural inclusion $\mathbb{N} \hookrightarrow R$.

frobenius_neg theorem

: frobenius R p (-x) = -frobenius R p x

Full source

lemma frobenius_neg : frobenius R p (-x) = -frobenius R p x := map_neg ..

Frobenius Endomorphism Preserves Negation: $\text{Frob}_p(-x) = -\text{Frob}_p(x)$

Informal description

Let $R$ be a commutative ring with exponential characteristic $p$. The Frobenius endomorphism $\text{Frob}_p : R \to R$ satisfies $\text{Frob}_p(-x) = -\text{Frob}_p(x)$ for all $x \in R$.

frobenius_sub theorem

: frobenius R p (x - y) = frobenius R p x - frobenius R p y

Full source

lemma frobenius_sub : frobenius R p (x - y) = frobenius R p x - frobenius R p y := map_sub ..

Frobenius Endomorphism Preserves Subtraction: $\text{Frob}_p(x - y) = \text{Frob}_p(x) - \text{Frob}_p(y)$

Informal description

Let $R$ be a commutative ring with exponential characteristic $p$. The Frobenius endomorphism $\text{Frob}_p : R \to R$ satisfies $\text{Frob}_p(x - y) = \text{Frob}_p(x) - \text{Frob}_p(y)$ for all $x, y \in R$.

Mathlib.Algebra.CharP.Frobenius

Tags

Implementation notes