ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>DivisionSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>CharZero R<VAR>f : α → α<VAR>x : α<VAR>h : Function.IsFixedPt f x<VAR>g : α → M<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>birkhoffAverage R f g n x = g x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>DivisionRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : α → α<VAR>g : α → M<VAR>n : ℕ<VAR>x : α<GOAL>birkhoffAverage R f g n (f x) - birkhoffAverage R f g n x = (↑n)⁻¹ • (g (f^[n] x) - g x)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>p : ℕ<GOAL>pNilradical R p ≤ nilradical R
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>p : ℕ<VAR>hp : 1 < p<GOAL>pNilradical R p = nilradical R
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>p : ℕ<VAR>hp : ¬1 < p<GOAL>pNilradical R p = ⊥
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>p : ℕ<VAR>hp : p ≤ 1<GOAL>pNilradical R p = ⊥
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>p : ℕ<VAR>hp : Nat.Prime p<GOAL>pNilradical R p = nilradical R
<VAR>R : Type u_1<VAR>CommSemiring R<GOAL>pNilradical R 1 = ⊥
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>p : ℕ<VAR>x : R<GOAL>x ∈ pNilradical R p ↔ ∃ n, x ^ p ^ n = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>p : ℕ<VAR>ExpChar R p<VAR>x y : R<GOAL>x - y ∈ pNilradical R p ↔ ∃ n, x ^ p ^ n = y ^ p ^ n
<VAR>R : Type u_1<VAR>CommRing R<VAR>p : ℕ<VAR>ExpChar R p<VAR>h : pNilradical R p = ⊥<VAR>n : ℕ<GOAL>Function.Injective fun x => x ^ p ^ n
<VAR>R : Type u_1<VAR>CommRing R<VAR>p : ℕ<VAR>ExpChar R p<VAR>h : Function.Injective ⇑(frobenius R p)<GOAL>pNilradical R p = ⊥
<VAR>R : Type u_1<VAR>CommRing R<VAR>p : ℕ<VAR>ExpChar R p<VAR>PerfectRing R p<GOAL>pNilradical R p = ⊥
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>CommSemiring K<VAR>CommSemiring L<VAR>i : K →+* L<VAR>p : ℕ<VAR>self : IsPRadical i p<GOAL>RingHom.ker i ≤ pNilradical K p
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>CommSemiring K<VAR>CommSemiring L<VAR>i : K →+* L<VAR>p : ℕ<VAR>self : IsPRadical i p<VAR>x : L<GOAL>∃ n y, i y = x ^ p ^ n
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>CommSemiring K<VAR>CommSemiring L<VAR>i : K →+* L<VAR>p : ℕ<GOAL>IsPRadical i p ↔ (∀ (x : L), ∃ n y, i y = x ^ p ^ n) ∧ RingHom.ker i ≤ pNilradical K p
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>CommSemiring K<VAR>CommSemiring L<VAR>i : K →+* L<VAR>p : ℕ<VAR>IsPRadical i p<VAR>x : L<GOAL>∃ n y, i y = x ^ p ^ n
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>CommSemiring K<VAR>CommSemiring L<VAR>i : K →+* L<VAR>p : ℕ<VAR>IsPRadical i p<GOAL>RingHom.ker i ≤ pNilradical K p
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>CommSemiring K<VAR>CommSemiring L<VAR>i : K →+* L<VAR>p : ℕ<VAR>IsPRadical i p<GOAL>Ideal.comap i (pNilradical L p) = pNilradical K p
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>CommSemiring K<VAR>CommSemiring L<VAR>CommSemiring M<VAR>i : K →+* L<VAR>f : L →+* M<VAR>p : ℕ<VAR>IsPRadical i p<VAR>IsPRadical f p<GOAL>IsPRadical (f.comp i) p
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>CommSemiring K<VAR>CommSemiring L<VAR>i : K →+* L<VAR>p : ℕ<VAR>ExpChar L p<VAR>PerfectRing L p<GOAL>pNilradical K p ≤ RingHom.ker i
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>CommSemiring K<VAR>CommSemiring L<VAR>i : K →+* L<VAR>p : ℕ<VAR>ExpChar L p<VAR>PerfectRing L p<VAR>IsPerfectClosure i p<GOAL>RingHom.ker i = pNilradical K p
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>CommSemiring K<VAR>CommSemiring L<VAR>i : K →+* L<VAR>p : ℕ<VAR>IsPRadical i p<VAR>x : L<GOAL>∃ y, i y.2 = x ^ p ^ y.1
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>CommSemiring K<VAR>CommSemiring L<VAR>i : K →+* L<VAR>p : ℕ<VAR>ExpChar L p<VAR>IsPRadical i p<VAR>PerfectRing L p<VAR>x : L<GOAL>PerfectRing.liftAux i i p x = x
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>CommSemiring K<VAR>CommSemiring L<VAR>i : K →+* L<VAR>p : ℕ<VAR>ExpChar L p<VAR>IsPRadical i p<VAR>PerfectRing L p<GOAL>PerfectRing.liftAux i i p = id
<VAR>K : Type u_1<VAR>M : Type u_3<VAR>CommSemiring K<VAR>CommSemiring M<VAR>j : K →+* M<VAR>p : ℕ<VAR>ExpChar M p<VAR>PerfectRing M p<VAR>x : K<GOAL>PerfectRing.liftAux (RingHom.id K) j p x = j x
<VAR>K : Type u_1<VAR>M : Type u_3<VAR>CommSemiring K<VAR>CommSemiring M<VAR>j : K →+* M<VAR>p : ℕ<VAR>ExpChar M p<VAR>PerfectRing M p<GOAL>PerfectRing.liftAux (RingHom.id K) j p = ⇑j
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>CommRing K<VAR>CommRing L<VAR>CommRing M<VAR>i : K →+* L<VAR>p : ℕ<VAR>ExpChar M p<VAR>IsPRadical i p<VAR>h : pNilradical M p = ⊥<GOAL>Function.Injective fun f => f.comp i
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>CommRing K<VAR>CommRing L<VAR>CommRing M<VAR>i : K →+* L<VAR>p : ℕ<VAR>ExpChar M p<VAR>IsPRadical i p<VAR>IsReduced M<GOAL>Function.Injective fun f => f.comp i
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>CommRing K<VAR>CommRing L<VAR>CommRing M<VAR>i : K →+* L<VAR>p : ℕ<VAR>ExpChar M p<VAR>IsPRadical i p<VAR>PerfectRing M p<GOAL>Function.Injective fun f => f.comp i
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>CommRing K<VAR>CommRing L<VAR>CommRing M<VAR>i : K →+* L<VAR>j : K →+* M<VAR>p : ℕ<VAR>ExpChar K p<VAR>ExpChar M p<VAR>PerfectRing M p<VAR>IsPRadical i p<VAR>x : L<VAR>n : ℕ<VAR>y : K<VAR>h : i y = x ^ p ^ n<GOAL>PerfectRing.liftAux i j p x = (iterateFrobeniusEquiv M p n).symm (j y)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>CommRing K<VAR>CommRing L<VAR>CommRing M<VAR>i : K →+* L<VAR>j : K →+* M<VAR>p : ℕ<VAR>ExpChar K p<VAR>ExpChar L p<VAR>ExpChar M p<VAR>PerfectRing M p<VAR>IsPRadical i p<VAR>x : L<VAR>n : ℕ<VAR>y : K<VAR>h : i y = x ^ p ^ n<GOAL>(PerfectRing.lift i j p) x = (iterateFrobeniusEquiv M p n).symm (j y)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>CommRing K<VAR>CommRing L<VAR>CommRing M<VAR>i : K →+* L<VAR>j : K →+* M<VAR>p : ℕ<VAR>ExpChar K p<VAR>ExpChar L p<VAR>ExpChar M p<VAR>PerfectRing M p<VAR>IsPRadical i p<VAR>x : K<GOAL>(PerfectRing.lift i j p) (i x) = j x
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>CommRing K<VAR>CommRing L<VAR>CommRing M<VAR>i : K →+* L<VAR>j : K →+* M<VAR>p : ℕ<VAR>ExpChar K p<VAR>ExpChar L p<VAR>ExpChar M p<VAR>PerfectRing M p<VAR>IsPRadical i p<GOAL>(PerfectRing.lift i j p).comp i = j
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>CommRing K<VAR>CommRing L<VAR>i : K →+* L<VAR>p : ℕ<VAR>ExpChar K p<VAR>ExpChar L p<VAR>IsPRadical i p<VAR>PerfectRing L p<VAR>x : L<GOAL>(PerfectRing.lift i i p) x = x
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>CommRing K<VAR>CommRing L<VAR>i : K →+* L<VAR>p : ℕ<VAR>ExpChar K p<VAR>ExpChar L p<VAR>IsPRadical i p<VAR>PerfectRing L p<GOAL>PerfectRing.lift i i p = RingHom.id L
<VAR>K : Type u_1<VAR>M : Type u_3<VAR>CommRing K<VAR>CommRing M<VAR>j : K →+* M<VAR>p : ℕ<VAR>ExpChar K p<VAR>ExpChar M p<VAR>PerfectRing M p<VAR>x : K<GOAL>(PerfectRing.lift (RingHom.id K) j p) x = j x
<VAR>K : Type u_1<VAR>M : Type u_3<VAR>CommRing K<VAR>CommRing M<VAR>j : K →+* M<VAR>p : ℕ<VAR>ExpChar K p<VAR>ExpChar M p<VAR>PerfectRing M p<GOAL>PerfectRing.lift (RingHom.id K) j p = j
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>CommRing K<VAR>CommRing L<VAR>CommRing M<VAR>i : K →+* L<VAR>f : L →+* M<VAR>p : ℕ<VAR>ExpChar K p<VAR>ExpChar L p<VAR>ExpChar M p<VAR>PerfectRing M p<VAR>IsPRadical i p<GOAL>PerfectRing.lift i (f.comp i) p = f
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>CommRing K<VAR>CommRing L<VAR>CommRing M<VAR>i : K →+* L<VAR>f : L →+* M<VAR>p : ℕ<VAR>ExpChar K p<VAR>ExpChar L p<VAR>ExpChar M p<VAR>PerfectRing M p<VAR>IsPRadical i p<VAR>x : L<GOAL>(PerfectRing.lift i (f.comp i) p) x = f x
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>CommRing K<VAR>CommRing L<VAR>CommRing M<VAR>i : K →+* L<VAR>j : K →+* M<VAR>p : ℕ<VAR>ExpChar K p<VAR>ExpChar L p<VAR>ExpChar M p<VAR>PerfectRing M p<VAR>IsPRadical i p<GOAL>(PerfectRing.liftEquiv M i p) j = PerfectRing.lift i j p
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>CommRing K<VAR>CommRing L<VAR>CommRing M<VAR>i : K →+* L<VAR>f : L →+* M<VAR>p : ℕ<VAR>ExpChar K p<VAR>ExpChar L p<VAR>ExpChar M p<VAR>PerfectRing M p<VAR>IsPRadical i p<GOAL>(PerfectRing.liftEquiv M i p).symm f = f.comp i
<VAR>K : Type u_1<VAR>M : Type u_3<VAR>CommRing K<VAR>CommRing M<VAR>j : K →+* M<VAR>p : ℕ<VAR>ExpChar K p<VAR>ExpChar M p<VAR>PerfectRing M p<GOAL>(PerfectRing.liftEquiv M (RingHom.id K) p) j = j
<VAR>K : Type u_1<VAR>M : Type u_3<VAR>CommRing K<VAR>CommRing M<VAR>p : ℕ<VAR>ExpChar K p<VAR>ExpChar M p<VAR>PerfectRing M p<GOAL>PerfectRing.liftEquiv M (RingHom.id K) p = Equiv.refl (K →+* M)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing K<VAR>CommRing L<VAR>CommRing M<VAR>CommRing N<VAR>i : K →+* L<VAR>j : K →+* M<VAR>k : K →+* N<VAR>p : ℕ<VAR>ExpChar K p<VAR>ExpChar L p<VAR>ExpChar M p<VAR>ExpChar N p<VAR>PerfectRing M p<VAR>IsPRadical i p<VAR>PerfectRing N p<VAR>IsPRadical j p<GOAL>(PerfectRing.lift j k p).comp (PerfectRing.lift i j p) = PerfectRing.lift i k p
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing K<VAR>CommRing L<VAR>CommRing M<VAR>CommRing N<VAR>i : K →+* L<VAR>j : K →+* M<VAR>k : K →+* N<VAR>p : ℕ<VAR>ExpChar K p<VAR>ExpChar L p<VAR>ExpChar M p<VAR>ExpChar N p<VAR>PerfectRing M p<VAR>IsPRadical i p<VAR>PerfectRing N p<VAR>IsPRadical j p<VAR>x : L<GOAL>(PerfectRing.lift j k p) ((PerfectRing.lift i j p) x) = (PerfectRing.lift i k p) x
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>CommRing K<VAR>CommRing L<VAR>CommRing M<VAR>i : K →+* L<VAR>j : K →+* M<VAR>p : ℕ<VAR>ExpChar K p<VAR>ExpChar L p<VAR>ExpChar M p<VAR>PerfectRing M p<VAR>IsPRadical i p<VAR>IsPRadical j p<VAR>PerfectRing L p<VAR>x : L<GOAL>(PerfectRing.lift j i p) ((PerfectRing.lift i j p) x) = x
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>CommRing K<VAR>CommRing L<VAR>CommRing M<VAR>i : K →+* L<VAR>j : K →+* M<VAR>p : ℕ<VAR>ExpChar K p<VAR>ExpChar L p<VAR>ExpChar M p<VAR>PerfectRing M p<VAR>IsPRadical i p<VAR>IsPRadical j p<VAR>PerfectRing L p<GOAL>(PerfectRing.lift j i p).comp (PerfectRing.lift i j p) = RingHom.id L
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing K<VAR>CommRing L<VAR>CommRing M<VAR>CommRing N<VAR>i : K →+* L<VAR>j : K →+* M<VAR>g : L →+* N<VAR>p : ℕ<VAR>ExpChar K p<VAR>ExpChar L p<VAR>ExpChar M p<VAR>ExpChar N p<VAR>PerfectRing M p<VAR>IsPRadical i p<VAR>IsPRadical g p<VAR>IsPRadical (g.comp i) p<GOAL>PerfectRing.lift g (PerfectRing.lift i j p) p = PerfectRing.lift (g.comp i) j p
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing K<VAR>CommRing L<VAR>CommRing M<VAR>CommRing N<VAR>i : K →+* L<VAR>j : K →+* M<VAR>g : L →+* N<VAR>p : ℕ<VAR>ExpChar K p<VAR>ExpChar L p<VAR>ExpChar M p<VAR>ExpChar N p<VAR>PerfectRing M p<VAR>IsPRadical i p<VAR>IsPRadical g p<VAR>IsPRadical (g.comp i) p<VAR>x : N<GOAL>(PerfectRing.lift g (PerfectRing.lift i j p) p) x = (PerfectRing.lift (g.comp i) j p) x
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing K<VAR>CommRing L<VAR>CommRing M<VAR>CommRing N<VAR>i : K →+* L<VAR>j : K →+* M<VAR>g : L →+* N<VAR>p : ℕ<VAR>ExpChar K p<VAR>ExpChar L p<VAR>ExpChar M p<VAR>ExpChar N p<VAR>PerfectRing M p<VAR>IsPRadical i p<VAR>IsPRadical g p<VAR>IsPRadical (g.comp i) p<GOAL>(PerfectRing.liftEquiv M g p) ((PerfectRing.liftEquiv M i p) j) = (PerfectRing.liftEquiv M (g.comp i) p) j
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing K<VAR>CommRing L<VAR>CommRing M<VAR>CommRing N<VAR>i : K →+* L<VAR>g : L →+* N<VAR>p : ℕ<VAR>ExpChar K p<VAR>ExpChar L p<VAR>ExpChar M p<VAR>ExpChar N p<VAR>PerfectRing M p<VAR>IsPRadical i p<VAR>IsPRadical g p<VAR>IsPRadical (g.comp i) p<GOAL>(PerfectRing.liftEquiv M i p).trans (PerfectRing.liftEquiv M g p) = PerfectRing.liftEquiv M (g.comp i) p
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>CommRing K<VAR>CommRing L<VAR>CommRing M<VAR>i : K →+* L<VAR>j : K →+* M<VAR>p : ℕ<VAR>ExpChar K p<VAR>ExpChar L p<VAR>ExpChar M p<VAR>PerfectRing L p<VAR>IsPerfectClosure i p<VAR>PerfectRing M p<VAR>IsPerfectClosure j p<GOAL>(IsPerfectClosure.equiv i j p).toRingHom = PerfectRing.lift i j p
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>CommRing K<VAR>CommRing L<VAR>CommRing M<VAR>i : K →+* L<VAR>j : K →+* M<VAR>p : ℕ<VAR>ExpChar K p<VAR>ExpChar L p<VAR>ExpChar M p<VAR>PerfectRing L p<VAR>IsPerfectClosure i p<VAR>PerfectRing M p<VAR>IsPerfectClosure j p<GOAL>(IsPerfectClosure.equiv i j p).symm = IsPerfectClosure.equiv j i p
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>CommRing K<VAR>CommRing L<VAR>CommRing M<VAR>i : K →+* L<VAR>j : K →+* M<VAR>p : ℕ<VAR>ExpChar K p<VAR>ExpChar L p<VAR>ExpChar M p<VAR>PerfectRing L p<VAR>IsPerfectClosure i p<VAR>PerfectRing M p<VAR>IsPerfectClosure j p<GOAL>(IsPerfectClosure.equiv i j p).symm.toRingHom = PerfectRing.lift j i p
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>CommRing K<VAR>CommRing L<VAR>CommRing M<VAR>i : K →+* L<VAR>j : K →+* M<VAR>p : ℕ<VAR>ExpChar K p<VAR>ExpChar L p<VAR>ExpChar M p<VAR>PerfectRing L p<VAR>IsPerfectClosure i p<VAR>PerfectRing M p<VAR>IsPerfectClosure j p<VAR>x : L<VAR>n : ℕ<VAR>y : K<VAR>h : i y = x ^ p ^ n<GOAL>(IsPerfectClosure.equiv i j p) x = (iterateFrobeniusEquiv M p n).symm (j y)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>CommRing K<VAR>CommRing L<VAR>CommRing M<VAR>i : K →+* L<VAR>j : K →+* M<VAR>p : ℕ<VAR>ExpChar K p<VAR>ExpChar L p<VAR>ExpChar M p<VAR>PerfectRing L p<VAR>IsPerfectClosure i p<VAR>PerfectRing M p<VAR>IsPerfectClosure j p<VAR>x : M<VAR>n : ℕ<VAR>y : K<VAR>h : j y = x ^ p ^ n<GOAL>(IsPerfectClosure.equiv i j p).symm x = (iterateFrobeniusEquiv L p n).symm (i y)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>CommRing K<VAR>CommRing L<VAR>i : K →+* L<VAR>p : ℕ<VAR>ExpChar K p<VAR>ExpChar L p<VAR>PerfectRing L p<VAR>IsPerfectClosure i p<VAR>x : L<GOAL>(IsPerfectClosure.equiv i i p) x = x
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>CommRing K<VAR>CommRing L<VAR>i : K →+* L<VAR>p : ℕ<VAR>ExpChar K p<VAR>ExpChar L p<VAR>PerfectRing L p<VAR>IsPerfectClosure i p<GOAL>IsPerfectClosure.equiv i i p = RingEquiv.refl L
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>CommRing K<VAR>CommRing L<VAR>CommRing M<VAR>i : K →+* L<VAR>j : K →+* M<VAR>p : ℕ<VAR>ExpChar K p<VAR>ExpChar L p<VAR>ExpChar M p<VAR>PerfectRing L p<VAR>IsPerfectClosure i p<VAR>PerfectRing M p<VAR>IsPerfectClosure j p<VAR>x : K<GOAL>(IsPerfectClosure.equiv i j p) (i x) = j x
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>CommRing K<VAR>CommRing L<VAR>CommRing M<VAR>i : K →+* L<VAR>j : K →+* M<VAR>p : ℕ<VAR>ExpChar K p<VAR>ExpChar L p<VAR>ExpChar M p<VAR>PerfectRing L p<VAR>IsPerfectClosure i p<VAR>PerfectRing M p<VAR>IsPerfectClosure j p<GOAL>(↑(IsPerfectClosure.equiv i j p)).comp i = j
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing K<VAR>CommRing L<VAR>CommRing M<VAR>CommRing N<VAR>i : K →+* L<VAR>j : K →+* M<VAR>k : K →+* N<VAR>p : ℕ<VAR>ExpChar K p<VAR>ExpChar L p<VAR>ExpChar M p<VAR>ExpChar N p<VAR>PerfectRing L p<VAR>IsPerfectClosure i p<VAR>PerfectRing M p<VAR>IsPerfectClosure j p<VAR>PerfectRing N p<VAR>IsPerfectClosure k p<VAR>x : L<GOAL>(IsPerfectClosure.equiv j k p) ((IsPerfectClosure.equiv i j p) x) = (IsPerfectClosure.equiv i k p) x
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>CommRing K<VAR>CommRing L<VAR>CommRing M<VAR>CommRing N<VAR>i : K →+* L<VAR>j : K →+* M<VAR>k : K →+* N<VAR>p : ℕ<VAR>ExpChar K p<VAR>ExpChar L p<VAR>ExpChar M p<VAR>ExpChar N p<VAR>PerfectRing L p<VAR>IsPerfectClosure i p<VAR>PerfectRing M p<VAR>IsPerfectClosure j p<VAR>PerfectRing N p<VAR>IsPerfectClosure k p<GOAL>(IsPerfectClosure.equiv i j p).trans (IsPerfectClosure.equiv j k p) = IsPerfectClosure.equiv i k p
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>CommRing K<VAR>CommRing L<VAR>CommRing M<VAR>i : K →+* L<VAR>j : K →+* M<VAR>p : ℕ<VAR>ExpChar K p<VAR>ExpChar L p<VAR>ExpChar M p<VAR>PerfectRing L p<VAR>IsPerfectClosure i p<VAR>PerfectRing M p<VAR>IsPerfectClosure j p<VAR>x : L<GOAL>(IsPerfectClosure.equiv j i p) ((IsPerfectClosure.equiv i j p) x) = x
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>CommRing K<VAR>CommRing L<VAR>CommRing M<VAR>i : K →+* L<VAR>j : K →+* M<VAR>p : ℕ<VAR>ExpChar K p<VAR>ExpChar L p<VAR>ExpChar M p<VAR>PerfectRing L p<VAR>IsPerfectClosure i p<VAR>PerfectRing M p<VAR>IsPerfectClosure j p<GOAL>(IsPerfectClosure.equiv i j p).trans (IsPerfectClosure.equiv j i p) = RingEquiv.refl L
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>p : ℕ<VAR>ExpChar K p<VAR>IsPRadical (algebraMap K L) p<GOAL>IsPurelyInseparable K L
<VAR>α : Type u_1<VAR>Fintype α<VAR>Field α<GOAL>IsPrimePow ‖α‖
<VAR>α : Type u_1<VAR>Fintype α<GOAL>Nonempty (Field α) ↔ IsPrimePow ‖α‖
<VAR>α : Type u_1<VAR>Fintype α<VAR>Ring α<GOAL>¬IsPrimePow ‖α‖ → ¬IsField α
<VAR>α : Type u<VAR>Infinite α<GOAL>Nonempty (Field α)
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>AddMonoid M<VAR>TopologicalSpace α<VAR>AddAction M α<VAR>self : AddAction.IsMinimal M α<VAR>x : α<GOAL>Dense (AddAction.orbit M x)
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Monoid M<VAR>TopologicalSpace α<VAR>MulAction M α<VAR>self : MulAction.IsMinimal M α<VAR>x : α<GOAL>Dense (MulAction.orbit M x)
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>Monoid M<VAR>TopologicalSpace α<VAR>MulAction M α<VAR>MulAction.IsMinimal M α<VAR>x : α<GOAL>Dense (MulAction.orbit M x)
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>AddMonoid M<VAR>TopologicalSpace α<VAR>AddAction M α<VAR>AddAction.IsMinimal M α<VAR>x : α<GOAL>Dense (AddAction.orbit M x)
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>AddMonoid M<VAR>TopologicalSpace α<VAR>AddAction M α<VAR>AddAction.IsMinimal M α<VAR>x : α<GOAL>DenseRange fun c => c +ᵥ x
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>Monoid M<VAR>TopologicalSpace α<VAR>MulAction M α<VAR>MulAction.IsMinimal M α<VAR>x : α<GOAL>DenseRange fun c => c • x
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>Monoid M<VAR>TopologicalSpace α<VAR>MulAction M α<VAR>MulAction.IsMinimal M α<VAR>x : α<VAR>U : Set α<VAR>hUo : IsOpen U<VAR>hne : U.Nonempty<GOAL>∃ c, c • x ∈ U
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>AddMonoid M<VAR>TopologicalSpace α<VAR>AddAction M α<VAR>AddAction.IsMinimal M α<VAR>x : α<VAR>U : Set α<VAR>hUo : IsOpen U<VAR>hne : U.Nonempty<GOAL>∃ c, c +ᵥ x ∈ U
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>Monoid M<VAR>TopologicalSpace α<VAR>MulAction M α<VAR>MulAction.IsMinimal M α<VAR>U : Set α<VAR>hUo : IsOpen U<VAR>hne : U.Nonempty<GOAL>⋃ c, (fun x => c • x) ⁻¹' U = Set.univ
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>AddMonoid M<VAR>TopologicalSpace α<VAR>AddAction M α<VAR>AddAction.IsMinimal M α<VAR>U : Set α<VAR>hUo : IsOpen U<VAR>hne : U.Nonempty<GOAL>⋃ c, (fun x => c +ᵥ x) ⁻¹' U = Set.univ
<VAR>G : Type u_2<VAR>α : Type u_3<VAR>AddGroup G<VAR>TopologicalSpace α<VAR>AddAction G α<VAR>AddAction.IsMinimal G α<VAR>U : Set α<VAR>hUo : IsOpen U<VAR>hne : U.Nonempty<GOAL>⋃ g, g +ᵥ U = Set.univ
<VAR>G : Type u_2<VAR>α : Type u_3<VAR>Group G<VAR>TopologicalSpace α<VAR>MulAction G α<VAR>MulAction.IsMinimal G α<VAR>U : Set α<VAR>hUo : IsOpen U<VAR>hne : U.Nonempty<GOAL>⋃ g, g • U = Set.univ
<VAR>G : Type u_2<VAR>α : Type u_3<VAR>Group G<VAR>TopologicalSpace α<VAR>MulAction G α<VAR>MulAction.IsMinimal G α<VAR>ContinuousConstSMul G α<VAR>K U : Set α<VAR>hK : IsCompact K<VAR>hUo : IsOpen U<VAR>hne : U.Nonempty<GOAL>∃ I, K ⊆ ⋃ g ∈ I, g • U
<VAR>G : Type u_2<VAR>α : Type u_3<VAR>AddGroup G<VAR>TopologicalSpace α<VAR>AddAction G α<VAR>AddAction.IsMinimal G α<VAR>ContinuousConstVAdd G α<VAR>K U : Set α<VAR>hK : IsCompact K<VAR>hUo : IsOpen U<VAR>hne : U.Nonempty<GOAL>∃ I, K ⊆ ⋃ g ∈ I, g +ᵥ U
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>AddMonoid M<VAR>TopologicalSpace α<VAR>AddAction M α<VAR>AddAction.IsMinimal M α<VAR>s : Set α<VAR>hne : s.Nonempty<VAR>hsmul : ∀ (c : M), c +ᵥ s ⊆ s<GOAL>Dense s
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>Monoid M<VAR>TopologicalSpace α<VAR>MulAction M α<VAR>MulAction.IsMinimal M α<VAR>s : Set α<VAR>hne : s.Nonempty<VAR>hsmul : ∀ (c : M), c • s ⊆ s<GOAL>Dense s
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>AddMonoid M<VAR>TopologicalSpace α<VAR>AddAction M α<VAR>AddAction.IsMinimal M α<VAR>s : Set α<VAR>hs : IsClosed s<VAR>hsmul : ∀ (c : M), c +ᵥ s ⊆ s<GOAL>s = ∅ ∨ s = Set.univ
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>Monoid M<VAR>TopologicalSpace α<VAR>MulAction M α<VAR>MulAction.IsMinimal M α<VAR>s : Set α<VAR>hs : IsClosed s<VAR>hsmul : ∀ (c : M), c • s ⊆ s<GOAL>s = ∅ ∨ s = Set.univ
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>Monoid M<VAR>TopologicalSpace α<VAR>MulAction M α<VAR>ContinuousConstSMul M α<GOAL>MulAction.IsMinimal M α ↔ ∀ (s : Set α), IsClosed s → (∀ (c : M), c • s ⊆ s) → s = ∅ ∨ s = Set.univ
<VAR>M : Type u_1<VAR>α : Type u_3<VAR>AddMonoid M<VAR>TopologicalSpace α<VAR>AddAction M α<VAR>ContinuousConstVAdd M α<GOAL>AddAction.IsMinimal M α ↔ ∀ (s : Set α), IsClosed s → (∀ (c : M), c +ᵥ s ⊆ s) → s = ∅ ∨ s = Set.univ
<VAR>α : Type u<VAR>x : α<GOAL>Function.IsFixedPt id x
<VAR>α : Type u<VAR>f : α → α<VAR>x : α<VAR>hf : Function.IsFixedPt f x<GOAL>f x = x
<VAR>α : Type u<VAR>f g : α → α<VAR>x : α<VAR>hf : Function.IsFixedPt f x<VAR>hg : Function.IsFixedPt g x<GOAL>Function.IsFixedPt (f ∘ g) x
<VAR>α : Type u<VAR>f : α → α<VAR>x : α<VAR>hf : Function.IsFixedPt f x<VAR>n : ℕ<GOAL>Function.IsFixedPt f^[n] x
<VAR>α : Type u<VAR>f g : α → α<VAR>x : α<VAR>hfg : Function.IsFixedPt (f ∘ g) x<VAR>hg : Function.IsFixedPt g x<GOAL>Function.IsFixedPt f x
<VAR>α : Type u<VAR>f g : α → α<VAR>x : α<VAR>hf : Function.IsFixedPt f x<VAR>h : Function.LeftInverse g f<GOAL>Function.IsFixedPt g x
<VAR>α : Type u<VAR>β : Type v<VAR>fa : α → α<VAR>fb : β → β<VAR>x : α<VAR>hx : Function.IsFixedPt fa x<VAR>g : α → β<VAR>h : Function.Semiconj g fa fb<GOAL>Function.IsFixedPt fb (g x)
<VAR>α : Type u<VAR>f : α → α<VAR>x : α<VAR>hx : Function.IsFixedPt f x<GOAL>Function.IsFixedPt f (f x)
<VAR>α : Type u<VAR>f : α → α<VAR>s : Set α<VAR>h : Function.IsFixedPt (Set.preimage f) s<VAR>n : ℕ<GOAL>Function.IsFixedPt (Set.preimage f^[n]) s
<VAR>α : Type u<VAR>f : α → α<VAR>s : Set α<VAR>h : Function.IsFixedPt (Set.image f) s<VAR>n : ℕ<GOAL>Function.IsFixedPt (Set.image f^[n]) s
<VAR>α : Type u<VAR>x : α<VAR>e : Equiv.Perm α<VAR>h : Function.IsFixedPt (⇑e) x<GOAL>Function.IsFixedPt (⇑(Equiv.symm e)) x
<VAR>α : Type u<VAR>x : α<VAR>e : Equiv.Perm α<VAR>h : Function.IsFixedPt (⇑e) x<GOAL>Function.IsFixedPt (⇑e⁻¹) x
<VAR>α : Type u<VAR>x : α<VAR>e : Equiv.Perm α<VAR>h : Function.IsFixedPt (⇑e) x<VAR>n : ℕ<GOAL>Function.IsFixedPt (⇑(e ^ n)) x
<VAR>α : Type u<VAR>x : α<VAR>e : Equiv.Perm α<VAR>h : Function.IsFixedPt (⇑e) x<VAR>n : ℤ<GOAL>Function.IsFixedPt (⇑(e ^ n)) x
<VAR>α : Type u<VAR>f : α → α<VAR>hf : Function.Injective f<VAR>x : α<GOAL>Function.IsFixedPt f (f x) ↔ Function.IsFixedPt f x
<VAR>α : Type u<VAR>f : α → α<VAR>x : α<GOAL>x ∈ Function.fixedPoints f ↔ Function.IsFixedPt f x
<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<GOAL>x ∈ Function.fixedPoints f ↔ f x = x
<VAR>α : Type u<GOAL>Function.fixedPoints id = Set.univ
<VAR>α : Type u<VAR>f : α → α<GOAL>Function.fixedPoints f ⊆ Set.range f
<VAR>α : Type u<VAR>β : Type v<VAR>fa : α → α<VAR>fb : β → β<VAR>g : α → β<VAR>h : Function.Semiconj g fa fb<GOAL>Set.MapsTo g (Function.fixedPoints fa) (Function.fixedPoints fb)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>g : β → α<GOAL>Set.InvOn f g (Function.fixedPoints (f ∘ g)) (Function.fixedPoints (g ∘ f))
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>g : β → α<GOAL>Set.MapsTo f (Function.fixedPoints (g ∘ f)) (Function.fixedPoints (f ∘ g))
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>g : β → α<GOAL>Set.BijOn g (Function.fixedPoints (f ∘ g)) (Function.fixedPoints (g ∘ f))
<VAR>α : Type u<VAR>f g : α → α<VAR>h : Function.Commute f g<GOAL>Set.InvOn f g (Function.fixedPoints (f ∘ g)) (Function.fixedPoints (f ∘ g))
<VAR>α : Type u<VAR>f g : α → α<VAR>h : Function.Commute f g<GOAL>Set.BijOn f (Function.fixedPoints (f ∘ g)) (Function.fixedPoints (f ∘ g))
<VAR>α : Type u<VAR>f g : α → α<VAR>h : Function.Commute f g<GOAL>Set.BijOn g (Function.fixedPoints (f ∘ g)) (Function.fixedPoints (f ∘ g))
<VAR>σ : Type u_1<VAR>n : ℕ<VAR>φ : MvPolynomial σ ℤ<GOAL>MvPolynomial.C ↑n ∣ φ ↔ (MvPolynomial.map (Int.castRingHom (ZMod n))) φ = 0
<VAR>σ : Type u_1<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>f : MvPolynomial σ (ZMod p)<GOAL>(frobenius (MvPolynomial σ (ZMod p)) p) f = (MvPolynomial.expand p) f
<VAR>σ : Type u_1<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>f : MvPolynomial σ (ZMod p)<GOAL>(MvPolynomial.expand p) f = f ^ p