ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>CommRing R<VAR>CommRing S<VAR>CommRing T<VAR>Algebra R S<VAR>Algebra R T<VAR>Algebra S T<VAR>IsScalarTower R S T<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>Finite ι<VAR>Finite κ<VAR>b : Basis ι R S<VAR>c : Basis κ S T<VAR>x : T<GOAL>(Algebra.trace R S) ((Algebra.trace S T) x) = (Algebra.trace R T) x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>CommRing R<VAR>CommRing S<VAR>CommRing T<VAR>Algebra R S<VAR>Algebra R T<VAR>Algebra S T<VAR>IsScalarTower R S T<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>Finite ι<VAR>Finite κ<VAR>b : Basis ι R S<VAR>c : Basis κ S T<GOAL>Algebra.trace R S ∘ₗ ↑R (Algebra.trace S T) = Algebra.trace R T
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>CommRing R<VAR>CommRing S<VAR>CommRing T<VAR>Algebra R S<VAR>Algebra R T<VAR>Algebra S T<VAR>IsScalarTower R S T<VAR>Module.Free R S<VAR>Module.Finite R S<VAR>Module.Free S T<VAR>Module.Finite S T<VAR>x : T<GOAL>(Algebra.trace R S) ((Algebra.trace S T) x) = (Algebra.trace R T) x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>CommRing R<VAR>CommRing S<VAR>CommRing T<VAR>Algebra R S<VAR>Algebra R T<VAR>Algebra S T<VAR>IsScalarTower R S T<VAR>Module.Free R S<VAR>Module.Finite R S<VAR>Module.Free S T<VAR>Module.Finite S T<GOAL>Algebra.trace R S ∘ₗ ↑R (Algebra.trace S T) = Algebra.trace R T
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>CommRing R<VAR>CommRing S<VAR>CommRing T<VAR>Algebra R S<VAR>Algebra R T<VAR>Module.Free R S<VAR>Module.Free R T<VAR>Module.Finite R S<VAR>Module.Finite R T<VAR>x : S × T<GOAL>(Algebra.trace R (S × T)) x = (Algebra.trace R S) x.1 + (Algebra.trace R T) x.2
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>CommRing R<VAR>CommRing S<VAR>CommRing T<VAR>Algebra R S<VAR>Algebra R T<VAR>Module.Free R S<VAR>Module.Free R T<VAR>Module.Finite R S<VAR>Module.Finite R T<GOAL>Algebra.trace R (S × T) = (Algebra.trace R S).coprod (Algebra.trace R T)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>x y : S<GOAL>((Algebra.traceForm R S) x) y = (Algebra.trace R S) (x * y)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<GOAL>(Algebra.traceForm R S).IsSymm
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>ι : Type w<VAR>Fintype ι<VAR>b : Basis ι R S<VAR>DecidableEq ι<VAR>i j : ι<GOAL>(BilinForm.toMatrix b) (Algebra.traceForm R S) i j = (Algebra.trace R S) (b i * b j)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>(WittVector.wittPolyProd p n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>(WittVector.wittPolyProdRemainder p n).vars ⊆ Finset.univ ×ˢ Finset.range n
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>(WittVector.remainder p n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>∑ i ∈ Finset.range (n + 1), ↑p ^ i * WittVector.wittMul p i ^ p ^ (n - i) = WittVector.wittPolyProd p n
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>↑p ^ n * WittVector.wittMul p n + WittVector.wittPolyProdRemainder p n = WittVector.wittPolyProd p n
<VAR>p n : ℕ<GOAL>WittVector.wittPolyProd p (n + 1) = -(↑p ^ (n + 1) * MvPolynomial.X (0, n + 1)) * (↑p ^ (n + 1) * MvPolynomial.X (1, n + 1)) + ↑p ^ (n + 1) * MvPolynomial.X (0, n + 1) * (MvPolynomial.rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) + ↑p ^ (n + 1) * MvPolynomial.X (1, n + 1) * (MvPolynomial.rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)) + WittVector.remainder p n
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>↑p ^ (n + 1) * WittVector.wittMul p (n + 1) = -(↑p ^ (n + 1) * MvPolynomial.X (0, n + 1)) * (↑p ^ (n + 1) * MvPolynomial.X (1, n + 1)) + ↑p ^ (n + 1) * MvPolynomial.X (0, n + 1) * (MvPolynomial.rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) + ↑p ^ (n + 1) * MvPolynomial.X (1, n + 1) * (MvPolynomial.rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)) + (WittVector.remainder p n - WittVector.wittPolyProdRemainder p (n + 1))
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>↑p ^ (n + 1) * WittVector.polyOfInterest p n = WittVector.remainder p n - WittVector.wittPolyProdRemainder p (n + 1)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>(↑p ^ (n + 1) * WittVector.polyOfInterest p n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>(WittVector.polyOfInterest p n).vars = (↑p ^ (n + 1) * (WittVector.wittMul p (n + 1) + ↑p ^ (n + 1) * MvPolynomial.X (0, n + 1) * MvPolynomial.X (1, n + 1) - MvPolynomial.X (0, n + 1) * (MvPolynomial.rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) - MvPolynomial.X (1, n + 1) * (MvPolynomial.rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)))).vars
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>(WittVector.polyOfInterest p n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>CommRing k<VAR>n : ℕ<VAR>x y : WittVector p k<GOAL>WittVector.peval (WittVector.polyOfInterest p n) ![fun i => x.coeff i, fun i => y.coeff i] = (x * y).coeff (n + 1) + ↑p ^ (n + 1) * x.coeff (n + 1) * y.coeff (n + 1) - y.coeff (n + 1) * ∑ i ∈ Finset.range (n + 1 + 1), ↑p ^ i * x.coeff i ^ p ^ (n + 1 - i) - x.coeff (n + 1) * ∑ i ∈ Finset.range (n + 1 + 1), ↑p ^ i * y.coeff i ^ p ^ (n + 1 - i)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>CommRing k<VAR>CharP k p<VAR>n : ℕ<VAR>x y : WittVector p k<GOAL>WittVector.peval (WittVector.polyOfInterest p n) ![fun i => x.coeff i, fun i => y.coeff i] = (x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>CommRing k<VAR>CharP k p<VAR>n : ℕ<GOAL>∃ f, ∀ (x y : WittVector p k), f (WittVector.truncateFun (n + 1) x) (WittVector.truncateFun (n + 1) y) = (x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>CommRing k<VAR>CharP k p<VAR>n : ℕ<GOAL>∃ f, ∀ (x y : WittVector p k), (x * y).coeff (n + 1) = x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1) + y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) + f (WittVector.truncateFun (n + 1) x) (WittVector.truncateFun (n + 1) y)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>CommRing k<VAR>CharP k p<VAR>n : ℕ<VAR>x y : WittVector p k<GOAL>(x * y).coeff (n + 1) = x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1) + y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) + WittVector.nthRemainder p n (WittVector.truncateFun (n + 1) x) (WittVector.truncateFun (n + 1) y)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>CommRing k<VAR>CharP k p<VAR>IsDomain k<VAR>n : ℕ<VAR>a₁ a₂ : WittVector p k<VAR>bs : Fin (n + 1) → k<VAR>ha₁ : a₁.coeff 0 ≠ 0<VAR>ha₂ : a₂.coeff 0 ≠ 0<GOAL>(WittVector.RecursionMain.succNthDefiningPoly p n a₁ a₂ bs).degree = ↑p
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>Field k<VAR>CharP k p<VAR>IsAlgClosed k<VAR>n : ℕ<VAR>a₁ a₂ : WittVector p k<VAR>bs : Fin (n + 1) → k<VAR>ha₁ : a₁.coeff 0 ≠ 0<VAR>ha₂ : a₂.coeff 0 ≠ 0<GOAL>∃ b, (WittVector.RecursionMain.succNthDefiningPoly p n a₁ a₂ bs).IsRoot b
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>Field k<VAR>CharP k p<VAR>IsAlgClosed k<VAR>n : ℕ<VAR>a₁ a₂ : WittVector p k<VAR>bs : Fin (n + 1) → k<VAR>ha₁ : a₁.coeff 0 ≠ 0<VAR>ha₂ : a₂.coeff 0 ≠ 0<GOAL>(WittVector.RecursionMain.succNthDefiningPoly p n a₁ a₂ bs).IsRoot (WittVector.RecursionMain.succNthVal p n a₁ a₂ bs ha₁ ha₂)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>Field k<VAR>CharP k p<VAR>IsAlgClosed k<VAR>n : ℕ<VAR>a₁ a₂ : WittVector p k<VAR>bs : Fin (n + 1) → k<VAR>ha₁ : a₁.coeff 0 ≠ 0<VAR>ha₂ : a₂.coeff 0 ≠ 0<GOAL>WittVector.RecursionMain.succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) + a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) + WittVector.nthRemainder p n (fun v => bs v ^ p) (WittVector.truncateFun (n + 1) a₁) = WittVector.RecursionMain.succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) + a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) + WittVector.nthRemainder p n bs (WittVector.truncateFun (n + 1) a₂)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>Field k<VAR>IsAlgClosed k<VAR>a₁ a₂ : WittVector p k<GOAL>∃ x, x ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>Field k<VAR>IsAlgClosed k<VAR>a₁ a₂ : WittVector p k<GOAL>WittVector.RecursionBase.solution p a₁ a₂ ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>Field k<VAR>IsAlgClosed k<VAR>a₁ a₂ : WittVector p k<VAR>ha₁ : a₁.coeff 0 ≠ 0<VAR>ha₂ : a₂.coeff 0 ≠ 0<GOAL>WittVector.RecursionBase.solution p a₁ a₂ ≠ 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>Field k<VAR>IsAlgClosed k<VAR>a₁ : WittVector p k<VAR>ha₁ : a₁.coeff 0 ≠ 0<VAR>a₂ : WittVector p k<GOAL>WittVector.RecursionBase.solution p a₁ a₂ ^ p * a₁.coeff 0 = WittVector.RecursionBase.solution p a₁ a₂ * a₂.coeff 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>Field k<VAR>CharP k p<VAR>IsAlgClosed k<VAR>a₁ a₂ : WittVector p k<VAR>ha₁ : a₁.coeff 0 ≠ 0<VAR>ha₂ : a₂.coeff 0 ≠ 0<GOAL>WittVector.frobeniusRotation p ha₁ ha₂ ≠ 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>Field k<VAR>CharP k p<VAR>IsAlgClosed k<VAR>a₁ a₂ : WittVector p k<VAR>ha₁ : a₁.coeff 0 ≠ 0<VAR>ha₂ : a₂.coeff 0 ≠ 0<GOAL>WittVector.frobenius (WittVector.frobeniusRotation p ha₁ ha₂) * a₁ = WittVector.frobeniusRotation p ha₁ ha₂ * a₂
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>Field k<VAR>CharP k p<VAR>IsAlgClosed k<VAR>m n : ℕ<VAR>r' q' : WittVector p k<VAR>hr' : r'.coeff 0 ≠ 0<VAR>hq' : q'.coeff 0 ≠ 0<VAR>hq : ↑p ^ n * q' ∈ nonZeroDivisors (WittVector p k)<GOAL>let b := WittVector.frobeniusRotation p hr' hq';
(IsFractionRing.fieldEquivOfRingEquiv (WittVector.frobeniusEquiv p k)) ((algebraMap (WittVector p k) (FractionRing (WittVector p k))) b) * Localization.mk (↑p ^ m * r') ⟨↑p ^ n * q', hq⟩ = ↑p ^ (↑m - ↑n) * (algebraMap (WittVector p k) (FractionRing (WittVector p k))) b
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>Field k<VAR>CharP k p<VAR>IsAlgClosed k<VAR>a : FractionRing (WittVector p k)<VAR>ha : a ≠ 0<GOAL>∃ b, b ≠ 0 ∧ ∃ m, (IsFractionRing.fieldEquivOfRingEquiv (WittVector.frobeniusEquiv p k)) b * a = ↑p ^ m * b
<VAR>p : ℕ<VAR>α : Type u_4<VAR>β : Type u_5<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>Function.Injective (WittVector.mapFun f)
<VAR>p : ℕ<VAR>α : Type u_4<VAR>β : Type u_5<VAR>f : α → β<VAR>hf : Function.Surjective f<GOAL>Function.Surjective (WittVector.mapFun f)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<GOAL>WittVector.mapFun (⇑f) 0 = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<GOAL>WittVector.mapFun (⇑f) 1 = 1
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>x y : 𝕎 R<GOAL>WittVector.mapFun (⇑f) (x + y) = WittVector.mapFun (⇑f) x + WittVector.mapFun (⇑f) y
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>x y : 𝕎 R<GOAL>WittVector.mapFun (⇑f) (x - y) = WittVector.mapFun (⇑f) x - WittVector.mapFun (⇑f) y
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>x y : 𝕎 R<GOAL>WittVector.mapFun (⇑f) (x * y) = WittVector.mapFun (⇑f) x * WittVector.mapFun (⇑f) y
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>x : 𝕎 R<GOAL>WittVector.mapFun (⇑f) (-x) = -WittVector.mapFun (⇑f) x
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>n : ℕ<VAR>x : 𝕎 R<GOAL>WittVector.mapFun (⇑f) (n • x) = n • WittVector.mapFun (⇑f) x
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>z : ℤ<VAR>x : 𝕎 R<GOAL>WittVector.mapFun (⇑f) (z • x) = z • WittVector.mapFun (⇑f) x
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>x : 𝕎 R<VAR>n : ℕ<GOAL>WittVector.mapFun (⇑f) (x ^ n) = WittVector.mapFun (⇑f) x ^ n
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>n : ℕ<GOAL>WittVector.mapFun ⇑f ↑n = ↑n
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>n : ℤ<GOAL>WittVector.mapFun ⇑f ↑n = ↑n
<VAR>p : ℕ<VAR>R : Type u_6<VAR>i : Fin 0<VAR>j : ℕ<GOAL>(![] i).coeff j = ![] i j
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<GOAL>WittVector.ghostFun 0 = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<GOAL>WittVector.ghostFun 1 = 1
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>x y : 𝕎 R<GOAL>WittVector.ghostFun (x + y) = WittVector.ghostFun x + WittVector.ghostFun y
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>i : ℕ<GOAL>WittVector.ghostFun ↑i = ↑i
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>x y : 𝕎 R<GOAL>WittVector.ghostFun (x - y) = WittVector.ghostFun x - WittVector.ghostFun y
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>x y : 𝕎 R<GOAL>WittVector.ghostFun (x * y) = WittVector.ghostFun x * WittVector.ghostFun y
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>x : 𝕎 R<GOAL>WittVector.ghostFun (-x) = -WittVector.ghostFun x
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>i : ℤ<GOAL>WittVector.ghostFun ↑i = ↑i
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>m : ℕ<VAR>x : 𝕎 R<GOAL>WittVector.ghostFun (m • x) = m • WittVector.ghostFun x
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>m : ℤ<VAR>x : 𝕎 R<GOAL>WittVector.ghostFun (m • x) = m • WittVector.ghostFun x
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>x : 𝕎 R<VAR>m : ℕ<GOAL>WittVector.ghostFun (x ^ m) = WittVector.ghostFun x ^ m
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<GOAL>Function.Injective ⇑(WittVector.map f)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Surjective ⇑(WittVector.map f)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>x : 𝕎 R<VAR>n : ℕ<GOAL>((WittVector.map f) x).coeff n = f (x.coeff n)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>n : ℕ<VAR>x : 𝕎 R<GOAL>(WittVector.ghostComponent n) x = (MvPolynomial.aeval x.coeff) (W_ ℤ n)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>x : 𝕎 R<VAR>n : ℕ<GOAL>WittVector.ghostMap x n = (WittVector.ghostComponent n) x
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>Invertible ↑p<GOAL>↑(WittVector.ghostEquiv p R) = WittVector.ghostMap
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>Invertible ↑p<GOAL>Function.Bijective ⇑WittVector.ghostMap
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>x : 𝕎 R<GOAL>WittVector.constantCoeff x = x.coeff 0
<VAR>K : Type u<VAR>Field K<VAR>self : ValuationSubring K<VAR>x : K<GOAL>x ∈ self.carrier ∨ x⁻¹ ∈ self.carrier
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<VAR>x : K<GOAL>x ∈ A.carrier ↔ x ∈ A
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<VAR>x : K<GOAL>x ∈ A.toSubring ↔ x ∈ A
<VAR>K : Type u<VAR>Field K<VAR>A B : ValuationSubring K<VAR>h : ∀ (x : K), x ∈ A ↔ x ∈ B<GOAL>A = B
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<GOAL>0 ∈ A
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<GOAL>1 ∈ A
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<VAR>x y : K<GOAL>x ∈ A → y ∈ A → x + y ∈ A
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<VAR>x y : K<GOAL>x ∈ A → y ∈ A → x * y ∈ A
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<VAR>x : K<GOAL>x ∈ A → -x ∈ A
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<VAR>x : K<GOAL>x ∈ A ∨ x⁻¹ ∈ A
<VAR>K : Type u<VAR>Field K<GOAL>Function.Injective ValuationSubring.toSubring
<VAR>K : Type u<VAR>Field K<VAR>x : K<GOAL>x ∈ ⊤
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<GOAL>A ≤ ⊤
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<VAR>a : ↥A<GOAL>(algebraMap (↥A) K) a = ↑a
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<VAR>a : ↥A<GOAL>A.valuation ↑a ≤ 1
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<VAR>x : K<VAR>h : A.valuation x ≤ 1<GOAL>x ∈ A
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<VAR>x : K<GOAL>A.valuation x ≤ 1 ↔ x ∈ A
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<VAR>x y : K<GOAL>A.valuation x = A.valuation y ↔ ∃ a, ↑↑a * y = x
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<VAR>x y : K<GOAL>A.valuation x ≤ A.valuation y ↔ ∃ a, ↑a * y = x
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<GOAL>Function.Surjective ⇑A.valuation
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<VAR>a : (↥A)ˣ<GOAL>A.valuation ↑↑a = 1
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<VAR>a : ↥A<GOAL>IsUnit a ↔ A.valuation ↑a = 1
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<VAR>a : ↥A<GOAL>A.valuation ↑a < 1 ∨ A.valuation ↑a = 1
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<VAR>a : ↥A<GOAL>a ∈ LocalRing.maximalIdeal ↥A ↔ A.valuation ↑a < 1
<VAR>K : Type u<VAR>Field K<VAR>R : Subring K<VAR>hR : ∀ (x : K), x ∈ R ∨ x⁻¹ ∈ R<VAR>x : K<GOAL>x ∈ ValuationSubring.ofSubring R hR ↔ x ∈ R
<VAR>K : Type u<VAR>Field K<VAR>R S : ValuationSubring K<VAR>h : R ≤ S<GOAL>Monotone ⇑(R.mapOfLE S h)
<VAR>K : Type u<VAR>Field K<VAR>R S : ValuationSubring K<VAR>h : R ≤ S<GOAL>⇑(R.mapOfLE S h) ∘ ⇑R.valuation = ⇑S.valuation
<VAR>K : Type u<VAR>Field K<VAR>R S : ValuationSubring K<VAR>h : R ≤ S<VAR>x : K<GOAL>(R.mapOfLE S h) (R.valuation x) = S.valuation x
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<VAR>P : Ideal ↥A<VAR>P.IsPrime<GOAL>A ≤ A.ofPrime P
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<VAR>P : Ideal ↥A<VAR>P.IsPrime<VAR>x : ↥A<GOAL>(A.ofPrime P).valuation ↑x = 1 ↔ x ∈ P.primeCompl
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<VAR>P : Ideal ↥A<VAR>P.IsPrime<GOAL>A.idealOfLE (A.ofPrime P) ⋯ = P
<VAR>K : Type u<VAR>Field K<VAR>R S : ValuationSubring K<VAR>h : R ≤ S<GOAL>R.ofPrime (R.idealOfLE S h) = S
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<VAR>P Q : Ideal ↥A<VAR>P.IsPrime<VAR>Q.IsPrime<VAR>h : P ≤ Q<GOAL>A.ofPrime Q ≤ A.ofPrime P
<VAR>K : Type u<VAR>Field K<VAR>A R S : ValuationSubring K<VAR>hR : A ≤ R<VAR>hS : A ≤ S<VAR>h : R ≤ S<GOAL>A.idealOfLE S hS ≤ A.idealOfLE R hR
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<VAR>P : PrimeSpectrum ↥A<GOAL>↑(A.primeSpectrumEquiv P) = A.ofPrime P.asIdeal
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<VAR>S : { S // A ≤ S }<GOAL>(A.primeSpectrumEquiv.symm S).asIdeal = A.idealOfLE ↑S ⋯
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<VAR>P : PrimeSpectrum ↥A<GOAL>↑↑(A.primeSpectrumOrderEquiv P) = {x | ∃ a ∈ A, ∃ a_1, (∃ (x : a_1 ∈ A), ⟨a_1, ⋯⟩ ∈ P.asIdeal.primeCompl) ∧ x = a * a_1⁻¹}
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<VAR>S : { S // A ≤ S }<GOAL>↑((RelIso.symm A.primeSpectrumOrderEquiv) S).asIdeal = ⇑(A.inclusion ↑S ⋯) ⁻¹' ↑(LocalRing.maximalIdeal ↥↑S)
<VAR>K : Type u<VAR>Field K<VAR>Γ : Type u_1<VAR>LinearOrderedCommGroupWithZero Γ<VAR>v : Valuation K Γ<VAR>x : K<GOAL>x ∈ v.valuationSubring ↔ v x ≤ 1
<VAR>K : Type u<VAR>Field K<VAR>Γ₁ : Type u_2<VAR>Γ₂ : Type u_3<VAR>LinearOrderedCommGroupWithZero Γ₁<VAR>LinearOrderedCommGroupWithZero Γ₂<VAR>v₁ : Valuation K Γ₁<VAR>v₂ : Valuation K Γ₂<GOAL>v₁.IsEquiv v₂ ↔ v₁.valuationSubring = v₂.valuationSubring
<VAR>K : Type u<VAR>Field K<VAR>Γ : Type u_1<VAR>LinearOrderedCommGroupWithZero Γ<VAR>v : Valuation K Γ<GOAL>v.IsEquiv v.valuationSubring.valuation
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<GOAL>A.valuation.valuationSubring = A
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<VAR>x : Kˣ<GOAL>x ∈ A.unitGroup ↔ A.valuation ↑x = 1
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<VAR>a : ↥A.unitGroup<GOAL>↑↑(A.unitGroupMulEquiv a) = ↑↑a
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<VAR>a : (↥A)ˣ<GOAL>↑↑(A.unitGroupMulEquiv.symm a) = ↑↑a
<VAR>K : Type u<VAR>Field K<VAR>A B : ValuationSubring K<GOAL>A.unitGroup ≤ B.unitGroup ↔ A ≤ B
<VAR>K : Type u<VAR>Field K<GOAL>Function.Injective ValuationSubring.unitGroup
<VAR>K : Type u<VAR>Field K<VAR>A B : ValuationSubring K<GOAL>A = B ↔ A.unitGroup = B.unitGroup
<VAR>K : Type u<VAR>Field K<GOAL>StrictMono ValuationSubring.unitGroup
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<VAR>x : K<GOAL>x ∈ A.nonunits ↔ A.valuation x < 1
<VAR>K : Type u<VAR>Field K<VAR>A B : ValuationSubring K<GOAL>B.nonunits ≤ A.nonunits ↔ A ≤ B
<VAR>K : Type u<VAR>Field K<GOAL>Function.Injective ValuationSubring.nonunits
<VAR>K : Type u<VAR>Field K<VAR>A B : ValuationSubring K<GOAL>A.nonunits = B.nonunits ↔ A = B
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<VAR>a : ↥A<GOAL>↑a ∈ A.nonunits ↔ a ∈ LocalRing.maximalIdeal ↥A
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<GOAL>A.nonunits ≤ A.toSubsemigroup
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<GOAL>↑A.nonunits ⊆ ↑A
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<VAR>a : K<GOAL>a ∈ A.nonunits ↔ ∃ (ha : a ∈ A), ⟨a, ha⟩ ∈ LocalRing.maximalIdeal ↥A
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<GOAL>Subtype.val '' ↑(LocalRing.maximalIdeal ↥A) = ↑A.nonunits
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<GOAL>A.principalUnitGroup ≤ A.unitGroup
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<VAR>x : Kˣ<GOAL>x ∈ A.principalUnitGroup ↔ A.valuation (↑x - 1) < 1
<VAR>K : Type u<VAR>Field K<VAR>A B : ValuationSubring K<GOAL>B.principalUnitGroup ≤ A.principalUnitGroup ↔ A ≤ B
<VAR>K : Type u<VAR>Field K<GOAL>Function.Injective ValuationSubring.principalUnitGroup
<VAR>K : Type u<VAR>Field K<VAR>A B : ValuationSubring K<GOAL>A = B ↔ A.principalUnitGroup = B.principalUnitGroup
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<VAR>x : ↥A.unitGroup<GOAL>↑x ∈ A.principalUnitGroup ↔ A.unitGroupMulEquiv x ∈ (Units.map ↑(LocalRing.residue ↥A)).ker
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<VAR>a : ↥A.principalUnitGroup<GOAL>↑↑↑(A.principalUnitGroupEquiv a) = ↑↑a
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<VAR>a : ↥(Units.map ↑(LocalRing.residue ↥A)).ker<GOAL>↑↑(A.principalUnitGroupEquiv.symm a) = ↑↑↑a
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<VAR>x : ↥A.unitGroup<GOAL>↑(A.unitGroupToResidueFieldUnits x) = (Ideal.Quotient.mk (LocalRing.maximalIdeal ↥A)) ↑(A.unitGroupMulEquiv x)
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<GOAL>A.unitGroupToResidueFieldUnits.ker = Subgroup.comap A.unitGroup.subtype A.principalUnitGroup
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<GOAL>Function.Surjective ⇑A.unitGroupToResidueFieldUnits
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<GOAL>A.unitsModPrincipalUnitsEquivResidueFieldUnits.toMonoidHom.comp (QuotientGroup.mk' (Subgroup.comap A.unitGroup.subtype A.principalUnitGroup)) = A.unitGroupToResidueFieldUnits
<VAR>K : Type u<VAR>Field K<VAR>A : ValuationSubring K<VAR>x : ↥A.unitGroup<GOAL>A.unitsModPrincipalUnitsEquivResidueFieldUnits.toMonoidHom ↑x = A.unitGroupToResidueFieldUnits x
<VAR>K : Type u<VAR>Field K<VAR>G : Type u_1<VAR>Group G<VAR>MulSemiringAction G K<VAR>g : G<VAR>S : ValuationSubring K<GOAL>↑(g • S) = g • ↑S
<VAR>K : Type u<VAR>Field K<VAR>G : Type u_1<VAR>Group G<VAR>MulSemiringAction G K<VAR>g : G<VAR>S : ValuationSubring K<GOAL>(g • S).toSubring = g • S.toSubring
<VAR>K : Type u<VAR>Field K<VAR>G : Type u_1<VAR>Group G<VAR>MulSemiringAction G K<VAR>g : G<VAR>x : K<VAR>S : ValuationSubring K<GOAL>x ∈ S → g • x ∈ g • S