ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>LinearOrderedCommGroupWithZero Γ'₀<VAR>v : Valuation K Γ₀<VAR>v' : Valuation K Γ'₀<GOAL>v.IsEquiv v' ↔ ∀ {x : K}, v (x - 1) < 1 ↔ v' (x - 1) < 1
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>LinearOrderedCommGroupWithZero Γ'₀<VAR>v : Valuation K Γ₀<VAR>v' : Valuation K Γ'₀<GOAL>[v.IsEquiv v', ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1, ∀ {x : K}, v x = 1 ↔ v' x = 1, ∀ {x : K}, v x < 1 ↔ v' x < 1, ∀ {x : K}, v (x - 1) < 1 ↔ v' (x - 1) < 1].TFAE
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>CommRing R<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x : R<GOAL>x ∈ v.supp ↔ v x = 0
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>CommRing R<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>a : R<VAR>s : R<VAR>h : s ∈ v.supp<GOAL>v (a + s) = v a
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>CommRing R<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>S : Type u_7<VAR>CommRing S<VAR>f : S →+* R<GOAL>(Valuation.comap f v).supp = Ideal.comap f v.supp
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedAddCommMonoidWithTop Γ₀<VAR>f : R → Γ₀<VAR>h0 : f 0 = ⊤<VAR>h1 : f 1 = 0<VAR>hadd : ∀ (x y : R), min (f x) (f y) ≤ f (x + y)<VAR>hmul : ∀ (x y : R), f (x * y) = f x + f y<VAR>r : R<GOAL>(AddValuation.of f h0 h1 hadd hmul) r = f r
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedAddCommMonoidWithTop Γ₀<VAR>v : AddValuation R Γ₀<VAR>r : R<GOAL>v.valuation r = Multiplicative.ofAdd (OrderDual.toDual (v r))
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedAddCommMonoidWithTop Γ₀<VAR>v : AddValuation R Γ₀<GOAL>v 0 = ⊤
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedAddCommMonoidWithTop Γ₀<VAR>v : AddValuation R Γ₀<GOAL>v 1 = 0
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedAddCommMonoidWithTop Γ₀<VAR>v : AddValuation R Γ₀<VAR>x y : R<GOAL>v (x * y) = v x + v y
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedAddCommMonoidWithTop Γ₀<VAR>v : AddValuation R Γ₀<VAR>x y : R<GOAL>min (v x) (v y) ≤ v (x + y)
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedAddCommMonoidWithTop Γ₀<VAR>v : AddValuation R Γ₀<VAR>x y : R<GOAL>v x ≤ v (x + y) ∨ v y ≤ v (x + y)
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedAddCommMonoidWithTop Γ₀<VAR>v : AddValuation R Γ₀<VAR>x y : R<VAR>g : Γ₀<VAR>hx : g ≤ v x<VAR>hy : g ≤ v y<GOAL>g ≤ v (x + y)
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedAddCommMonoidWithTop Γ₀<VAR>v : AddValuation R Γ₀<VAR>x y : R<VAR>g : Γ₀<VAR>hx : g < v x<VAR>hy : g < v y<GOAL>g < v (x + y)
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedAddCommMonoidWithTop Γ₀<VAR>v : AddValuation R Γ₀<VAR>ι : Type u_6<VAR>s : Finset ι<VAR>f : ι → R<VAR>g : Γ₀<VAR>hf : ∀ i ∈ s, g ≤ v (f i)<GOAL>g ≤ v (∑ i ∈ s, f i)
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedAddCommMonoidWithTop Γ₀<VAR>v : AddValuation R Γ₀<VAR>ι : Type u_6<VAR>s : Finset ι<VAR>f : ι → R<VAR>g : Γ₀<VAR>hg : g ≠ ⊤<VAR>hf : ∀ i ∈ s, g < v (f i)<GOAL>g < v (∑ i ∈ s, f i)
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedAddCommMonoidWithTop Γ₀<VAR>v : AddValuation R Γ₀<VAR>ι : Type u_6<VAR>s : Finset ι<VAR>f : ι → R<VAR>g : Γ₀<VAR>hg : g < ⊤<VAR>hf : ∀ i ∈ s, g < v (f i)<GOAL>g < v (∑ i ∈ s, f i)
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedAddCommMonoidWithTop Γ₀<VAR>v : AddValuation R Γ₀<VAR>x : R<VAR>n : ℕ<GOAL>v (x ^ n) = n • v x
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedAddCommMonoidWithTop Γ₀<VAR>v₁ v₂ : AddValuation R Γ₀<VAR>h : ∀ (r : R), v₁ r = v₂ r<GOAL>v₁ = v₂
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedAddCommMonoidWithTop Γ₀<VAR>v₁ v₂ : AddValuation R Γ₀<GOAL>v₁ = v₂ ↔ ∀ (r : R), v₁ r = v₂ r
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>Γ₀ : Type u_4<VAR>LinearOrderedAddCommMonoidWithTop Γ₀<VAR>Nontrivial Γ₀<VAR>v : AddValuation K Γ₀<VAR>x : K<GOAL>v x = ⊤ ↔ x = 0
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>Γ₀ : Type u_4<VAR>LinearOrderedAddCommMonoidWithTop Γ₀<VAR>Nontrivial Γ₀<VAR>v : AddValuation K Γ₀<VAR>x : K<GOAL>v x ≠ ⊤ ↔ x ≠ 0
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedAddCommMonoidWithTop Γ₀<VAR>v : AddValuation R Γ₀<GOAL>AddValuation.comap (RingHom.id R) v = v
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedAddCommMonoidWithTop Γ₀<VAR>v : AddValuation R Γ₀<VAR>S₁ : Type u_6<VAR>S₂ : Type u_7<VAR>Ring S₁<VAR>Ring S₂<VAR>f : S₁ →+* S₂<VAR>g : S₂ →+* R<GOAL>AddValuation.comap (g.comp f) v = AddValuation.comap f (AddValuation.comap g v)
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>Γ₀ : Type u_4<VAR>LinearOrderedAddCommGroupWithTop Γ₀<VAR>v : AddValuation K Γ₀<VAR>x : K<GOAL>v x⁻¹ = -v x
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>Γ₀ : Type u_4<VAR>LinearOrderedAddCommGroupWithTop Γ₀<VAR>v : AddValuation K Γ₀<VAR>x y : K<GOAL>v (x / y) = v x - v y
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>LinearOrderedAddCommGroupWithTop Γ₀<VAR>Ring R<VAR>v : AddValuation R Γ₀<VAR>x : R<GOAL>v (-x) = v x
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>LinearOrderedAddCommGroupWithTop Γ₀<VAR>Ring R<VAR>v : AddValuation R Γ₀<VAR>x y : R<GOAL>v (x - y) = v (y - x)
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>LinearOrderedAddCommGroupWithTop Γ₀<VAR>Ring R<VAR>v : AddValuation R Γ₀<VAR>x y : R<GOAL>min (v x) (v y) ≤ v (x - y)
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>LinearOrderedAddCommGroupWithTop Γ₀<VAR>Ring R<VAR>v : AddValuation R Γ₀<VAR>x y : R<VAR>g : Γ₀<VAR>hx : g ≤ v x<VAR>hy : g ≤ v y<GOAL>g ≤ v (x - y)
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>LinearOrderedAddCommGroupWithTop Γ₀<VAR>Ring R<VAR>v : AddValuation R Γ₀<VAR>x y : R<VAR>h : v x ≠ v y<GOAL>v (x + y) = min (v x) (v y)
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>LinearOrderedAddCommGroupWithTop Γ₀<VAR>Ring R<VAR>v : AddValuation R Γ₀<VAR>x y : R<VAR>h : v x < v y<GOAL>v (x + y) = v x
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>LinearOrderedAddCommGroupWithTop Γ₀<VAR>Ring R<VAR>v : AddValuation R Γ₀<VAR>x y : R<VAR>hx : v y < v x<GOAL>v (x + y) = v y
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>LinearOrderedAddCommGroupWithTop Γ₀<VAR>Ring R<VAR>v : AddValuation R Γ₀<VAR>x y : R<VAR>hx : v x < v y<GOAL>v (x - y) = v x
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>LinearOrderedAddCommGroupWithTop Γ₀<VAR>Ring R<VAR>v : AddValuation R Γ₀<VAR>x y : R<VAR>hx : v y < v x<GOAL>v (x - y) = v y
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>LinearOrderedAddCommGroupWithTop Γ₀<VAR>Ring R<VAR>v : AddValuation R Γ₀<VAR>x y : R<VAR>h : v x < v (y - x)<GOAL>v y = v x
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>LinearOrderedAddCommMonoidWithTop Γ₀<VAR>Ring R<VAR>v : AddValuation R Γ₀<GOAL>v.IsEquiv v
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>LinearOrderedAddCommMonoidWithTop Γ₀<VAR>LinearOrderedAddCommMonoidWithTop Γ'₀<VAR>Ring R<VAR>v₁ : AddValuation R Γ₀<VAR>v₂ : AddValuation R Γ'₀<VAR>h : v₁.IsEquiv v₂<GOAL>v₂.IsEquiv v₁
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>LinearOrderedAddCommMonoidWithTop Γ₀<VAR>LinearOrderedAddCommMonoidWithTop Γ'₀<VAR>Ring R<VAR>Γ''₀ : Type u_6<VAR>LinearOrderedAddCommMonoidWithTop Γ''₀<VAR>v₁ : AddValuation R Γ₀<VAR>v₂ : AddValuation R Γ'₀<VAR>v₃ : AddValuation R Γ''₀<VAR>h₁₂ : v₁.IsEquiv v₂<VAR>h₂₃ : v₂.IsEquiv v₃<GOAL>v₁.IsEquiv v₃
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>LinearOrderedAddCommMonoidWithTop Γ₀<VAR>Ring R<VAR>v v' : AddValuation R Γ₀<VAR>h : v = v'<GOAL>v.IsEquiv v'
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>LinearOrderedAddCommMonoidWithTop Γ₀<VAR>LinearOrderedAddCommMonoidWithTop Γ'₀<VAR>Ring R<VAR>v v' : AddValuation R Γ₀<VAR>f : Γ₀ →+ Γ'₀<VAR>ht : f ⊤ = ⊤<VAR>hf : Monotone ⇑f<VAR>inf : Function.Injective ⇑f<VAR>h : v.IsEquiv v'<GOAL>(AddValuation.map f ht hf v).IsEquiv (AddValuation.map f ht hf v')
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>LinearOrderedAddCommMonoidWithTop Γ₀<VAR>LinearOrderedAddCommMonoidWithTop Γ'₀<VAR>Ring R<VAR>v₁ : AddValuation R Γ₀<VAR>v₂ : AddValuation R Γ'₀<VAR>S : Type u_7<VAR>Ring S<VAR>f : S →+* R<VAR>h : v₁.IsEquiv v₂<GOAL>(AddValuation.comap f v₁).IsEquiv (AddValuation.comap f v₂)
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>LinearOrderedAddCommMonoidWithTop Γ₀<VAR>LinearOrderedAddCommMonoidWithTop Γ'₀<VAR>Ring R<VAR>v₁ : AddValuation R Γ₀<VAR>v₂ : AddValuation R Γ'₀<VAR>h : v₁.IsEquiv v₂<VAR>r s : R<GOAL>v₁ r = v₁ s ↔ v₂ r = v₂ s
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>LinearOrderedAddCommMonoidWithTop Γ₀<VAR>LinearOrderedAddCommMonoidWithTop Γ'₀<VAR>Ring R<VAR>v₁ : AddValuation R Γ₀<VAR>v₂ : AddValuation R Γ'₀<VAR>h : v₁.IsEquiv v₂<VAR>r : R<GOAL>v₁ r ≠ ⊤ ↔ v₂ r ≠ ⊤
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>LinearOrderedAddCommMonoidWithTop Γ₀<VAR>CommRing R<VAR>v : AddValuation R Γ₀<VAR>x : R<GOAL>x ∈ v.supp ↔ v x = ⊤
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>LinearOrderedAddCommMonoidWithTop Γ₀<VAR>CommRing R<VAR>v : AddValuation R Γ₀<VAR>a : R<VAR>s : R<VAR>h : s ∈ v.supp<GOAL>v (a + s) = v a
<GOAL>RingHom.LocalizationPreserves @RingHom.FinitePresentation
<GOAL>RingHom.StableUnderComposition @RingHom.FinitePresentation
<GOAL>RingHom.HoldsForLocalizationAway @RingHom.FinitePresentation
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>CommRing R<VAR>CommRing S<VAR>CommRing A<VAR>Algebra R S<VAR>Algebra R A<VAR>Algebra.FinitePresentation R A<VAR>f : A →ₐ[R] S<VAR>hf : Function.Surjective ⇑f<VAR>t : Finset A<VAR>ht : Ideal.span ↑t = ⊤<VAR>H : ∀ (g : { x // x ∈ t }), Algebra.FinitePresentation R (Localization.Away (f ↑g))<GOAL>Algebra.FinitePresentation R S
<GOAL>RingHom.OfLocalizationSpanTarget @RingHom.FinitePresentation
<GOAL>RingHom.PropertyIsLocal @RingHom.FinitePresentation
<GOAL>RingHom.RespectsIso @RingHom.FinitePresentation
<GOAL>RingHom.StableUnderBaseChange @RingHom.FinitePresentation
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>CommRing k<VAR>CharP k p<VAR>a : kˣ<VAR>A : WittVector p k<VAR>hA : A.coeff 0 = ↑a<GOAL>↑(WittVector.mkUnit hA) = A
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>Field k<VAR>CharP k p<VAR>x : WittVector p k<VAR>hx : x.coeff 0 ≠ 0<GOAL>IsUnit x
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>Field k<VAR>CharP k p<GOAL>Irreducible ↑p
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>CommRing k<VAR>CharP k p<VAR>PerfectRing k p<VAR>a : WittVector p k<VAR>ha : a ≠ 0<GOAL>∃ m b, b.coeff 0 ≠ 0 ∧ a = ↑p ^ m * b
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>Field k<VAR>CharP k p<VAR>PerfectRing k p<VAR>a : WittVector p k<VAR>ha : a ≠ 0<GOAL>∃ m b, a = ↑p ^ m * ↑b
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>Field k<VAR>CharP k p<VAR>PerfectRing k p<GOAL>DiscreteValuationRing (WittVector p k)
<VAR>A : Type u<VAR>CommRing A<VAR>IsDomain A<VAR>self : ValuationRing A<VAR>a b : A<GOAL>∃ c, a * c = b ∨ b * c = a
<VAR>A : Type u<VAR>CommRing A<VAR>IsDomain A<VAR>ValuationRing A<VAR>a b : A<GOAL>∃ c, a * c = b ∨ b * c = a
<VAR>A : Type u<VAR>CommRing A<VAR>K : Type v<VAR>Field K<VAR>Algebra A K<VAR>IsDomain A<VAR>ValuationRing A<VAR>IsFractionRing A K<VAR>a b : ValuationRing.ValueGroup A K<GOAL>a ≤ b ∨ b ≤ a
<VAR>A : Type u<VAR>CommRing A<VAR>K : Type v<VAR>Field K<VAR>Algebra A K<VAR>IsDomain A<VAR>ValuationRing A<VAR>IsFractionRing A K<VAR>x : K<GOAL>x ∈ (ValuationRing.valuation A K).integer ↔ ∃ a, (algebraMap A K) a = x
<VAR>A : Type u<VAR>CommRing A<VAR>K : Type v<VAR>Field K<VAR>Algebra A K<VAR>IsDomain A<VAR>ValuationRing A<VAR>IsFractionRing A K<VAR>a : A<GOAL>↑((ValuationRing.equivInteger A K) a) = (algebraMap A K) a
<VAR>A : Type u<VAR>CommRing A<VAR>K : Type v<VAR>Field K<VAR>Algebra A K<VAR>IsDomain A<VAR>ValuationRing A<VAR>IsFractionRing A K<GOAL>(ValuationRing.valuation A K).integer = (algebraMap A K).range
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<GOAL>ValuationRing R ↔ IsTotal R fun x x_1 => x ∣ x_1
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<GOAL>ValuationRing R ↔ IsTotal (Ideal R) fun x x_1 => x ≤ x_1
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>h : ValuationRing R<VAR>x y : R<GOAL>x ∣ y ∨ y ∣ x
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>ValuationRing R<VAR>p q : R<VAR>hp : Irreducible p<VAR>hq : Irreducible q<GOAL>Associated p q
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<GOAL>ValuationRing R ↔ ∀ (x : K), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>h : ValuationRing R<VAR>x : K<GOAL>IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<GOAL>ValuationRing R ↔ LocalRing R ∧ IsBezout R
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<GOAL>[ValuationRing R, ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹, IsTotal R fun x x_1 => x ∣ x_1, IsTotal (Ideal R) fun x x_1 => x ≤ x_1, LocalRing R ∧ IsBezout R].TFAE
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>ValuationRing R<VAR>CommRing S<VAR>IsDomain S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<GOAL>ValuationRing S
<VAR>𝒪 : Type u<VAR>K : Type v<VAR>Γ : Type w<VAR>CommRing 𝒪<VAR>IsDomain 𝒪<VAR>Field K<VAR>Algebra 𝒪 K<VAR>LinearOrderedCommGroupWithZero Γ<VAR>v : Valuation K Γ<VAR>hh : v.Integers 𝒪<GOAL>ValuationRing 𝒪
<VAR>𝒪 : Type u<VAR>K : Type v<VAR>CommRing 𝒪<VAR>IsDomain 𝒪<VAR>Field K<VAR>Algebra 𝒪 K<VAR>ValuationRing 𝒪<GOAL>IsFractionRing 𝒪 K ↔ (∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a) ∧ Function.Injective ⇑(algebraMap 𝒪 K)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>x : WittVector p R<VAR>n : ℕ<GOAL>x.verschiebungFun.coeff n = if n = 0 then 0 else x.coeff (n - 1)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>x : WittVector p R<GOAL>x.verschiebungFun.coeff 0 = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>x : WittVector p R<VAR>n : ℕ<GOAL>x.verschiebungFun.coeff n.succ = x.coeff n
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>x : WittVector p R<GOAL>(WittVector.ghostComponent 0) x.verschiebungFun = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>x : WittVector p R<VAR>n : ℕ<GOAL>(WittVector.ghostComponent (n + 1)) x.verschiebungFun = ↑p * (WittVector.ghostComponent n) x
<VAR>p : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>x : WittVector p R<VAR>n : ℕ<GOAL>(MvPolynomial.aeval x.coeff) (WittVector.verschiebungPoly n) = x.verschiebungFun.coeff n
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>WittVector.IsPoly p fun R _Rcr => ⇑WittVector.verschiebung
<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 : WittVector p R<GOAL>(WittVector.map f) (WittVector.verschiebung x) = WittVector.verschiebung ((WittVector.map f) x)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>x : WittVector p R<GOAL>(WittVector.ghostComponent 0) (WittVector.verschiebung x) = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>x : WittVector p R<VAR>n : ℕ<GOAL>(WittVector.ghostComponent (n + 1)) (WittVector.verschiebung x) = ↑p * (WittVector.ghostComponent n) x
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>x : WittVector p R<GOAL>(WittVector.verschiebung x).coeff 0 = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>x : WittVector p R<VAR>n : ℕ<GOAL>(WittVector.verschiebung x).coeff (n + 1) = x.coeff n
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>x : WittVector p R<VAR>n : ℕ<GOAL>(WittVector.verschiebung x).coeff n.succ = x.coeff n
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>x : WittVector p R<VAR>n : ℕ<GOAL>(MvPolynomial.aeval x.coeff) (WittVector.verschiebungPoly n) = (WittVector.verschiebung x).coeff n
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>(MvPolynomial.bind₁ WittVector.verschiebungPoly) (wittPolynomial p ℤ n) = if n = 0 then 0 else ↑p * wittPolynomial p ℤ (n - 1)
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>Subsingleton R<VAR>x : A<GOAL>Transcendental R x
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>self : Algebra.IsAlgebraic R A<VAR>x : A<GOAL>IsAlgebraic R x
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>self : Algebra.Transcendental R A<GOAL>∃ x, Transcendental R x
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<GOAL>Algebra.IsAlgebraic R A ↔ ∀ (x : A), IsAlgebraic R x
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<GOAL>Algebra.Transcendental R A ↔ ∃ x, Transcendental R x
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<GOAL>Algebra.Transcendental R A ↔ ¬Algebra.IsAlgebraic R A
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>S : Subalgebra R A<GOAL>S.IsAlgebraic ↔ Algebra.IsAlgebraic R ↥S
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<GOAL>Algebra.IsAlgebraic R A ↔ ⊤.IsAlgebraic
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>x : A<GOAL>IsAlgebraic R x ↔ ¬Function.Injective ⇑(Polynomial.aeval x)
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>x : A<GOAL>Transcendental R x ↔ Function.Injective ⇑(Polynomial.aeval x)
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>Nontrivial R<VAR>x : A<GOAL>IsIntegral R x → IsAlgebraic R x
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>Nontrivial R<GOAL>IsAlgebraic R 0
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>Nontrivial R<VAR>x : R<GOAL>IsAlgebraic R ((algebraMap R A) x)
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>Nontrivial R<GOAL>IsAlgebraic R 1
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>Nontrivial R<VAR>n : ℕ<GOAL>IsAlgebraic R ↑n
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>Nontrivial R<VAR>n : ℤ<GOAL>IsAlgebraic R ↑n
<VAR>R : Type u<VAR>A : Type v<VAR>DivisionRing A<VAR>Field R<VAR>Algebra R A<VAR>n : ℚ<GOAL>IsAlgebraic R ↑n
<VAR>R : Type u<VAR>A : Type v<VAR>Field R<VAR>Field A<VAR>Algebra R A<VAR>p : R[X]<VAR>x : A<VAR>hx : x ∈ p.rootSet A<GOAL>IsAlgebraic R x
<VAR>R : Type u<VAR>S : Type u_1<VAR>A : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Ring A<VAR>Algebra R A<VAR>Algebra R S<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>a : S<GOAL>IsAlgebraic R a → IsAlgebraic R ((algebraMap S A) a)
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>B : Type u_2<VAR>Ring B<VAR>Algebra R B<VAR>f : A →ₐ[R] B<VAR>a : A<VAR>h : IsAlgebraic R a<GOAL>IsAlgebraic R (f a)
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>B : Type u_2<VAR>Ring B<VAR>Algebra R B<VAR>f : A →ₐ[R] B<VAR>hf : Function.Injective ⇑f<VAR>a : A<GOAL>IsAlgebraic R (f a) ↔ IsAlgebraic R a
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>B : Type u_2<VAR>Ring B<VAR>Algebra R B<VAR>f : A →ₐ[R] B<VAR>hf : Function.Injective ⇑f<VAR>Algebra.IsAlgebraic R B<GOAL>Algebra.IsAlgebraic R A
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>B : Type u_2<VAR>Ring B<VAR>Algebra R B<VAR>e : A ≃ₐ[R] B<VAR>Algebra.IsAlgebraic R A<GOAL>Algebra.IsAlgebraic R B
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>B : Type u_2<VAR>Ring B<VAR>Algebra R B<VAR>e : A ≃ₐ[R] B<GOAL>Algebra.IsAlgebraic R A ↔ Algebra.IsAlgebraic R B
<VAR>R : Type u<VAR>S : Type u_1<VAR>A : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Ring A<VAR>Algebra R A<VAR>Algebra R S<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>a : S<VAR>h : Function.Injective ⇑(algebraMap S A)<GOAL>IsAlgebraic R ((algebraMap S A) a) ↔ IsAlgebraic R a
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>r : A<VAR>n : ℕ<VAR>hn : 0 < n<VAR>ht : IsAlgebraic R (r ^ n)<GOAL>IsAlgebraic R r
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>r : A<VAR>ht : Transcendental R r<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>Transcendental R (r ^ n)
<VAR>R : Type u<VAR>S : Type u_1<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>x : S<VAR>Invertible x<VAR>h : IsAlgebraic R x<GOAL>IsAlgebraic R ⅟x
<VAR>R : Type u<VAR>S : Type u_1<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>x : S<VAR>Invertible x<GOAL>IsAlgebraic R ⅟x ↔ IsAlgebraic R x
<VAR>R : Type u<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>x : K<GOAL>IsAlgebraic R x⁻¹ ↔ IsAlgebraic R x
<VAR>K : Type u<VAR>A : Type v<VAR>Field K<VAR>Ring A<VAR>Algebra K A<VAR>x : A<GOAL>IsAlgebraic K x ↔ IsIntegral K x
<VAR>K : Type u<VAR>A : Type v<VAR>Field K<VAR>Ring A<VAR>Algebra K A<GOAL>Algebra.IsAlgebraic K A ↔ Algebra.IsIntegral K A
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>CommRing R<VAR>CommRing S<VAR>Ring A<VAR>Algebra R S<VAR>Algebra S A<VAR>Algebra R A<VAR>IsScalarTower R S A<VAR>hinj : Function.Injective ⇑(algebraMap R S)<VAR>x : A<VAR>A_alg : IsAlgebraic R x<GOAL>IsAlgebraic S x
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>CommRing R<VAR>CommRing S<VAR>Ring A<VAR>Algebra R S<VAR>Algebra S A<VAR>Algebra R A<VAR>IsScalarTower R S A<VAR>hinj : Function.Injective ⇑(algebraMap R S)<VAR>Algebra.IsAlgebraic R A<GOAL>Algebra.IsAlgebraic S A
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>A : Type u_5<VAR>Field K<VAR>Field L<VAR>Ring A<VAR>Algebra K L<VAR>Algebra L A<VAR>Algebra K A<VAR>IsScalarTower K L A<VAR>x : A<VAR>A_alg : IsAlgebraic K x<GOAL>IsAlgebraic L x
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>A : Type u_5<VAR>Field K<VAR>Field L<VAR>Ring A<VAR>Algebra K L<VAR>Algebra L A<VAR>Algebra K A<VAR>IsScalarTower K L A<VAR>Algebra.IsAlgebraic K A<GOAL>Algebra.IsAlgebraic L A
<VAR>K : Type u_1<VAR>A : Type u_5<VAR>Field K<VAR>Ring A<VAR>Algebra K A<VAR>e : A<VAR>FiniteDimensional K A<GOAL>IsAlgebraic K e
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>A : Type u_5<VAR>Field K<VAR>Field L<VAR>Ring A<VAR>Algebra K L<VAR>Algebra L A<VAR>Algebra K A<VAR>IsScalarTower K L A<VAR>L_alg : Algebra.IsAlgebraic K L<VAR>A_alg : Algebra.IsAlgebraic L A<GOAL>Algebra.IsAlgebraic K A
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>CommRing K<VAR>Field L<VAR>Algebra K L<VAR>NoZeroSMulDivisors K L<VAR>Algebra.IsAlgebraic K L<VAR>f : L →ₐ[K] L<GOAL>Function.Bijective ⇑f
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>R : Type u_3<VAR>CommRing K<VAR>Field L<VAR>Algebra K L<VAR>NoZeroSMulDivisors K L<VAR>Field R<VAR>Algebra K R<VAR>Algebra.IsAlgebraic K L<VAR>f : L →ₐ[K] R<VAR>g : R →ₐ[K] L<GOAL>Function.Bijective ⇑f ∧ Function.Bijective ⇑g
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>R : Type u_3<VAR>CommRing K<VAR>Field L<VAR>Algebra K L<VAR>NoZeroSMulDivisors K L<VAR>Algebra.IsAlgebraic K L<VAR>Field R<VAR>Algebra K R<VAR>Algebra L R<VAR>IsScalarTower K L R<VAR>f : R →ₐ[K] L<GOAL>Function.Bijective ⇑f
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>R : Type u_3<VAR>CommRing K<VAR>Field L<VAR>Algebra K L<VAR>Field R<VAR>Algebra K R<VAR>NoZeroSMulDivisors K R<VAR>Algebra.IsAlgebraic K R<VAR>Algebra L R<VAR>IsScalarTower K L R<VAR>f : R →ₐ[K] L<GOAL>Function.Bijective ⇑f
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>CommRing K<VAR>Field L<VAR>Algebra K L<VAR>NoZeroSMulDivisors K L<VAR>Algebra.IsAlgebraic K L<VAR>ϕ : L →ₐ[K] L<GOAL>(Algebra.IsAlgebraic.algEquivEquivAlgHom K L).symm ϕ = AlgEquiv.ofBijective ϕ ⋯
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>CommRing K<VAR>Field L<VAR>Algebra K L<VAR>NoZeroSMulDivisors K L<VAR>Algebra.IsAlgebraic K L<VAR>ϕ : L ≃ₐ[K] L<GOAL>(Algebra.IsAlgebraic.algEquivEquivAlgHom K L) ϕ = ↑ϕ
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>FiniteDimensional K L<VAR>ϕ : L →ₐ[K] L<GOAL>Function.Bijective ⇑ϕ
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>CommRing S<VAR>Algebra R S<VAR>z : S<VAR>hz : IsAlgebraic R z<VAR>inj : ∀ (x : R), (algebraMap R S) x = 0 → x = 0<GOAL>∃ x y, y ≠ 0 ∧ z * (algebraMap R S) y = ↑x