ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>StrictOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>x y : M<GOAL>SameRay R (-x) (-y) ↔ SameRay R x y
<VAR>R : Type u_1<VAR>StrictOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>x y : M<GOAL>SameRay R (-x) y ↔ SameRay R x (-y)
<VAR>R : Type u_1<VAR>StrictOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>x : M<VAR>NoZeroSMulDivisors R M<VAR>r : R<VAR>hr : r < 0<VAR>h : SameRay R x (r • x)<GOAL>x = 0
<VAR>R : Type u_1<VAR>StrictOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>x : M<VAR>NoZeroSMulDivisors R M<VAR>h : SameRay R x (-x)<GOAL>x = 0
<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>R : Type u_4<VAR>v : RayVector R M<GOAL>↑(-v) = -↑v
<VAR>R : Type u_1<VAR>StrictOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>v₁ v₂ : RayVector R M<GOAL>-v₁ ≈ -v₂ ↔ v₁ ≈ v₂
<VAR>R : Type u_1<VAR>StrictOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>v : M<VAR>h : v ≠ 0<GOAL>-rayOfNeZero R v h = rayOfNeZero R (-v) ⋯
<VAR>R : Type u_1<VAR>StrictOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>x : Module.Ray R M<GOAL>x ≠ -x
<VAR>R : Type u_1<VAR>StrictOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>u : Rˣ<VAR>v : Module.Ray R M<GOAL>-u • v = -(u • v)
<VAR>R : Type u_1<VAR>StrictOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>u : Rˣ<VAR>hu : ↑u < 0<VAR>v : Module.Ray R M<GOAL>u • v = -v
<VAR>R : Type u_1<VAR>StrictOrderedCommRing R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>f : M ≃ₗ[R] N<VAR>v : Module.Ray R M<GOAL>(Module.Ray.map f) (-v) = -(Module.Ray.map f) v
<VAR>R : Type u_1<VAR>LinearOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>v₁ v₂ : M<VAR>h : v₁ ∈ MulAction.orbit (↥(Units.posSubgroup R)) v₂<GOAL>SameRay R v₁ v₂
<VAR>R : Type u_1<VAR>LinearOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>u : Rˣ<VAR>v : Module.Ray R M<GOAL>u⁻¹ • v = u • v
<VAR>R : Type u_1<VAR>LinearOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>v : M<VAR>r : R<GOAL>SameRay R v (r • v) ↔ 0 ≤ r ∨ v = 0
<VAR>R : Type u_1<VAR>LinearOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>v : M<VAR>hv : v ≠ 0<VAR>r : R<VAR>hr : r ≠ 0<GOAL>SameRay R v (r • v) ↔ 0 < r
<VAR>R : Type u_1<VAR>LinearOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>v : M<VAR>r : R<GOAL>SameRay R (r • v) v ↔ 0 ≤ r ∨ v = 0
<VAR>R : Type u_1<VAR>LinearOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>v : M<VAR>hv : v ≠ 0<VAR>r : R<VAR>hr : r ≠ 0<GOAL>SameRay R (r • v) v ↔ 0 < r
<VAR>R : Type u_1<VAR>LinearOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>v : M<VAR>r : R<GOAL>SameRay R (-v) (r • v) ↔ r ≤ 0 ∨ v = 0
<VAR>R : Type u_1<VAR>LinearOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>v : M<VAR>r : R<VAR>hv : v ≠ 0<VAR>hr : r ≠ 0<GOAL>SameRay R (-v) (r • v) ↔ r < 0
<VAR>R : Type u_1<VAR>LinearOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>v : M<VAR>r : R<GOAL>SameRay R (r • v) (-v) ↔ r ≤ 0 ∨ v = 0
<VAR>R : Type u_1<VAR>LinearOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>v : M<VAR>r : R<VAR>hv : v ≠ 0<VAR>hr : r ≠ 0<GOAL>SameRay R (r • v) (-v) ↔ r < 0
<VAR>R : Type u_1<VAR>LinearOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>u : Rˣ<VAR>v : Module.Ray R M<GOAL>u • v = v ↔ 0 < ↑u
<VAR>R : Type u_1<VAR>LinearOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>u : Rˣ<VAR>v : Module.Ray R M<GOAL>u • v = -v ↔ ↑u < 0
<VAR>R : Type u_1<VAR>LinearOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>x y : M<GOAL>SameRay R x y ∨ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]
<VAR>R : Type u_1<VAR>LinearOrderedCommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>x y : M<GOAL>SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]
<VAR>R : Type u_1<VAR>LinearOrderedField R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>x y : M<VAR>h : SameRay R x y<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>∃ r, 0 < r ∧ r • x = y
<VAR>R : Type u_1<VAR>LinearOrderedField R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>x y : M<VAR>h : SameRay R x y<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>∃ r, 0 < r ∧ x = r • y
<VAR>R : Type u_1<VAR>LinearOrderedField R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>x y : M<VAR>h : SameRay R x y<VAR>hx : x ≠ 0<GOAL>∃ r, 0 ≤ r ∧ r • x = y
<VAR>R : Type u_1<VAR>LinearOrderedField R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>x y : M<VAR>h : SameRay R x y<VAR>hy : y ≠ 0<GOAL>∃ r, 0 ≤ r ∧ x = r • y
<VAR>R : Type u_1<VAR>LinearOrderedField R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>v₁ v₂ : M<VAR>h : SameRay R v₁ v₂<GOAL>∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • (v₁ + v₂) ∧ v₂ = b • (v₁ + v₂)
<VAR>R : Type u_1<VAR>LinearOrderedField R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>v₁ v₂ : M<VAR>h : SameRay R v₁ v₂<GOAL>∃ u a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • u ∧ v₂ = b • u
<VAR>R : Type u_1<VAR>LinearOrderedField R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>x y : M<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>(∃ r, 0 < r ∧ r • x = y) ↔ SameRay R x y
<VAR>R : Type u_1<VAR>LinearOrderedField R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>x y : M<VAR>hx : x ≠ 0<GOAL>(∃ r, 0 < r ∧ r • x = y) ↔ SameRay R x y ∧ y ≠ 0
<VAR>R : Type u_1<VAR>LinearOrderedField R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>x y : M<VAR>hx : x ≠ 0<GOAL>(∃ r, 0 ≤ r ∧ r • x = y) ↔ SameRay R x y
<VAR>R : Type u_1<VAR>LinearOrderedField R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>x y : M<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>(∃ r, 0 < r ∧ x = r • y) ↔ SameRay R x y
<VAR>R : Type u_1<VAR>LinearOrderedField R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>x y : M<VAR>hy : y ≠ 0<GOAL>(∃ r, 0 < r ∧ x = r • y) ↔ SameRay R x y ∧ x ≠ 0
<VAR>R : Type u_1<VAR>LinearOrderedField R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>x y : M<VAR>hy : y ≠ 0<GOAL>(∃ r, 0 ≤ r ∧ x = r • y) ↔ SameRay R x y
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>Field K<VAR>Field L<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>Algebra B L<VAR>Algebra K L<VAR>Algebra A L<VAR>IsScalarTower A B L<VAR>IsScalarTower A K L<VAR>IsIntegralClosure B A L<VAR>FiniteDimensional K L<VAR>σ : L →ₐ[K] L<VAR>x : B<GOAL>(algebraMap B L) (((galRestrictHom A K L B) σ) x) = σ ((algebraMap B L) x)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>Field K<VAR>Field L<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>Algebra B L<VAR>Algebra K L<VAR>Algebra A L<VAR>IsScalarTower A B L<VAR>IsScalarTower A K L<VAR>IsIntegralClosure B A L<VAR>FiniteDimensional K L<VAR>σ : B →ₐ[A] B<VAR>x : B<GOAL>((galRestrictHom A K L B).symm σ) ((algebraMap B L) x) = (algebraMap B L) (σ x)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>Field K<VAR>Field L<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>Algebra B L<VAR>Algebra K L<VAR>Algebra A L<VAR>IsScalarTower A B L<VAR>IsScalarTower A K L<VAR>IsIntegralClosure B A L<VAR>FiniteDimensional K L<VAR>σ : L ≃ₐ[K] L<GOAL>↑((galRestrict A K L B) σ) = (galRestrictHom A K L B) ↑σ
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>Field K<VAR>Field L<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>Algebra B L<VAR>Algebra K L<VAR>Algebra A L<VAR>IsScalarTower A B L<VAR>IsScalarTower A K L<VAR>IsIntegralClosure B A L<VAR>FiniteDimensional K L<VAR>σ : L ≃ₐ[K] L<VAR>x : B<GOAL>((galRestrict A K L B) σ) x = ((galRestrictHom A K L B) ↑σ) x
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>Field K<VAR>Field L<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>Algebra B L<VAR>Algebra K L<VAR>Algebra A L<VAR>IsScalarTower A B L<VAR>IsScalarTower A K L<VAR>IsIntegralClosure B A L<VAR>FiniteDimensional K L<VAR>σ : L ≃ₐ[K] L<VAR>x : B<GOAL>(algebraMap B L) (((galRestrict A K L B) σ) x) = σ ((algebraMap B L) x)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>Field K<VAR>Field L<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>Algebra B L<VAR>Algebra K L<VAR>Algebra A L<VAR>IsScalarTower A B L<VAR>IsScalarTower A K L<VAR>IsIntegralClosure B A L<VAR>FiniteDimensional K L<VAR>IsGalois K L<VAR>IsIntegrallyClosed A<VAR>x : B<GOAL>∏ σ : L ≃ₐ[K] L, ((galRestrict A K L B) σ) x = (algebraMap A B) (IsIntegralClosure.mk' A ((Algebra.norm K) ((algebraMap B L) x)) ⋯)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>Field K<VAR>Field L<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>Algebra B L<VAR>Algebra K L<VAR>Algebra A L<VAR>IsScalarTower A B L<VAR>IsScalarTower A K L<VAR>IsIntegralClosure B A L<VAR>FiniteDimensional K L<VAR>IsIntegrallyClosed A<VAR>x : B<GOAL>(algebraMap A K) ((Algebra.intTraceAux A K L B) x) = (Algebra.trace K L) ((algebraMap B L) x)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>Field K<VAR>Field L<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>Algebra B L<VAR>Algebra K L<VAR>Algebra A L<VAR>IsScalarTower A B L<VAR>IsScalarTower A K L<VAR>IsIntegralClosure B A L<VAR>FiniteDimensional K L<VAR>IsDomain A<VAR>IsIntegrallyClosed A<VAR>IsDomain B<VAR>IsIntegrallyClosed B<VAR>Module.Finite A B<VAR>NoZeroSMulDivisors A B<VAR>x : B<GOAL>(algebraMap A K) ((Algebra.intTrace A B) x) = (Algebra.trace K L) ((algebraMap B L) x)
<VAR>A : Type u_1<VAR>B : Type u_4<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>IsDomain A<VAR>IsIntegrallyClosed A<VAR>IsDomain B<VAR>IsIntegrallyClosed B<VAR>Module.Finite A B<VAR>NoZeroSMulDivisors A B<VAR>x : B<GOAL>(algebraMap A (FractionRing A)) ((Algebra.intTrace A B) x) = (Algebra.trace (FractionRing A) (FractionRing B)) ((algebraMap B (FractionRing B)) x)
<VAR>A : Type u_1<VAR>B : Type u_4<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>IsDomain A<VAR>IsIntegrallyClosed A<VAR>IsDomain B<VAR>IsIntegrallyClosed B<VAR>Module.Finite A B<VAR>NoZeroSMulDivisors A B<VAR>Module.Free A B<GOAL>Algebra.intTrace A B = Algebra.trace A B
<VAR>A : Type u_1<VAR>B : Type u_4<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>Aₘ : Type u_5<VAR>Bₘ : Type u_6<VAR>CommRing Aₘ<VAR>CommRing Bₘ<VAR>Algebra Aₘ Bₘ<VAR>Algebra A Aₘ<VAR>Algebra B Bₘ<VAR>Algebra A Bₘ<VAR>IsScalarTower A Aₘ Bₘ<VAR>IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>IsLocalization M Aₘ<VAR>IsLocalization (Algebra.algebraMapSubmonoid B M) Bₘ<VAR>IsDomain A<VAR>IsIntegrallyClosed A<VAR>IsDomain B<VAR>IsIntegrallyClosed B<VAR>Module.Finite A B<VAR>NoZeroSMulDivisors A B<VAR>IsDomain Aₘ<VAR>IsIntegrallyClosed Aₘ<VAR>IsDomain Bₘ<VAR>IsIntegrallyClosed Bₘ<VAR>NoZeroSMulDivisors Aₘ Bₘ<VAR>Module.Finite Aₘ Bₘ<VAR>x : B<GOAL>(algebraMap A Aₘ) ((Algebra.intTrace A B) x) = (Algebra.intTrace Aₘ Bₘ) ((algebraMap B Bₘ) x)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>Field K<VAR>Field L<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>Algebra B L<VAR>Algebra K L<VAR>Algebra A L<VAR>IsScalarTower A B L<VAR>IsScalarTower A K L<VAR>IsIntegralClosure B A L<VAR>FiniteDimensional K L<VAR>IsIntegrallyClosed A<VAR>Algebra.IsSeparable K L<VAR>x : B<GOAL>(algebraMap A K) ((Algebra.intNormAux A K L B) x) = (Algebra.norm K) ((algebraMap B L) x)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>Field K<VAR>Field L<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>Algebra B L<VAR>Algebra K L<VAR>Algebra A L<VAR>IsScalarTower A B L<VAR>IsScalarTower A K L<VAR>IsIntegralClosure B A L<VAR>FiniteDimensional K L<VAR>IsDomain A<VAR>IsIntegrallyClosed A<VAR>IsDomain B<VAR>IsIntegrallyClosed B<VAR>Module.Finite A B<VAR>NoZeroSMulDivisors A B<VAR>Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>x : B<GOAL>(algebraMap A K) ((Algebra.intNorm A B) x) = (Algebra.norm K) ((algebraMap B L) x)
<VAR>A : Type u_1<VAR>B : Type u_4<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>IsDomain A<VAR>IsIntegrallyClosed A<VAR>IsDomain B<VAR>IsIntegrallyClosed B<VAR>Module.Finite A B<VAR>NoZeroSMulDivisors A B<VAR>Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>x : B<GOAL>(algebraMap A (FractionRing A)) ((Algebra.intNorm A B) x) = (Algebra.norm (FractionRing A)) ((algebraMap B (FractionRing B)) x)
<VAR>A : Type u_1<VAR>B : Type u_4<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>IsDomain A<VAR>IsIntegrallyClosed A<VAR>IsDomain B<VAR>IsIntegrallyClosed B<VAR>Module.Finite A B<VAR>NoZeroSMulDivisors A B<VAR>Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>Module.Free A B<GOAL>Algebra.intNorm A B = Algebra.norm A
<VAR>A : Type u_1<VAR>B : Type u_4<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>IsDomain A<VAR>IsIntegrallyClosed A<VAR>IsDomain B<VAR>IsIntegrallyClosed B<VAR>Module.Finite A B<VAR>NoZeroSMulDivisors A B<VAR>Algebra.IsSeparable (FractionRing A) (FractionRing B)<GOAL>(Algebra.intNorm A B) 0 = 0
<VAR>A : Type u_1<VAR>B : Type u_4<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>IsDomain A<VAR>IsIntegrallyClosed A<VAR>IsDomain B<VAR>IsIntegrallyClosed B<VAR>Module.Finite A B<VAR>NoZeroSMulDivisors A B<VAR>Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>x : B<GOAL>(Algebra.intNorm A B) x = 0 ↔ x = 0
<VAR>A : Type u_1<VAR>B : Type u_4<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>IsDomain A<VAR>IsIntegrallyClosed A<VAR>IsDomain B<VAR>IsIntegrallyClosed B<VAR>Module.Finite A B<VAR>NoZeroSMulDivisors A B<VAR>Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>x : B<GOAL>(Algebra.intNorm A B) x ≠ 0 ↔ x ≠ 0
<VAR>A : Type u_1<VAR>B : Type u_4<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>Aₘ : Type u_5<VAR>Bₘ : Type u_6<VAR>CommRing Aₘ<VAR>CommRing Bₘ<VAR>Algebra Aₘ Bₘ<VAR>Algebra A Aₘ<VAR>Algebra B Bₘ<VAR>Algebra A Bₘ<VAR>IsScalarTower A Aₘ Bₘ<VAR>IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>IsLocalization M Aₘ<VAR>IsLocalization (Algebra.algebraMapSubmonoid B M) Bₘ<VAR>IsDomain A<VAR>IsIntegrallyClosed A<VAR>IsDomain B<VAR>IsIntegrallyClosed B<VAR>Module.Finite A B<VAR>NoZeroSMulDivisors A B<VAR>Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>IsDomain Aₘ<VAR>IsIntegrallyClosed Aₘ<VAR>IsDomain Bₘ<VAR>IsIntegrallyClosed Bₘ<VAR>NoZeroSMulDivisors Aₘ Bₘ<VAR>Module.Finite Aₘ Bₘ<VAR>Algebra.IsSeparable (FractionRing Aₘ) (FractionRing Bₘ)<VAR>x : B<GOAL>(algebraMap A Aₘ) ((Algebra.intNorm A B) x) = (Algebra.intNorm Aₘ Bₘ) ((algebraMap B Bₘ) x)
<VAR>A : Type u_1<VAR>B : Type u_4<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>IsDomain A<VAR>IsIntegrallyClosed A<VAR>IsDomain B<VAR>IsIntegrallyClosed B<VAR>Module.Finite A B<VAR>NoZeroSMulDivisors A B<VAR>IsGalois (FractionRing A) (FractionRing B)<VAR>x : B<GOAL>(algebraMap A B) ((Algebra.intNorm A B) x) = ∏ σ : B ≃ₐ[A] B, σ x
<VAR>R : Type u<VAR>M : Type v<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>f : M →ₗ[R] M<GOAL>f.charpoly = ((LinearMap.toMatrix (Module.Free.chooseBasis R M) (Module.Free.chooseBasis R M)) f).charpoly
<VAR>R : Type u<VAR>M : Type v<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>f : M →ₗ[R] M<GOAL>f.charpoly.Monic
<VAR>R : Type u<VAR>M : Type v<VAR>CommRing R<VAR>Nontrivial R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>f : M →ₗ[R] M<VAR>StrongRankCondition R<GOAL>f.charpoly.natDegree = FiniteDimensional.finrank R M
<VAR>R : Type u<VAR>M : Type v<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>f : M →ₗ[R] M<GOAL>(Polynomial.aeval f) f.charpoly = 0
<VAR>R : Type u<VAR>M : Type v<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>f : M →ₗ[R] M<GOAL>IsIntegral R f
<VAR>K : Type u<VAR>M : Type v<VAR>Field K<VAR>AddCommGroup M<VAR>Module K M<VAR>FiniteDimensional K M<VAR>f : M →ₗ[K] M<GOAL>minpoly K f ∣ f.charpoly
<VAR>R : Type u<VAR>M : Type v<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>f : M →ₗ[R] M<VAR>p : R[X]<GOAL>(Polynomial.aeval f) p = (Polynomial.aeval f) (p %ₘ f.charpoly)
<VAR>R : Type u<VAR>M : Type v<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>f : M →ₗ[R] M<VAR>k : ℕ<GOAL>f ^ k = (Polynomial.aeval f) (Polynomial.X ^ k %ₘ f.charpoly)
<VAR>R : Type u<VAR>M : Type v<VAR>CommRing R<VAR>Nontrivial R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>f : M →ₗ[R] M<VAR>hf : Function.Injective ⇑f<GOAL>(minpoly R f).coeff 0 ≠ 0
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>OrderedRing k<VAR>OrderedAddCommGroup E<VAR>Module k E<VAR>OrderedSMul k E<VAR>a a' b : E<VAR>r : k<VAR>ha : a ≤ a'<VAR>hr : r ≤ 1<GOAL>(AffineMap.lineMap a b) r ≤ (AffineMap.lineMap a' b) r
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>OrderedRing k<VAR>OrderedAddCommGroup E<VAR>Module k E<VAR>OrderedSMul k E<VAR>a a' b : E<VAR>r : k<VAR>ha : a < a'<VAR>hr : r < 1<GOAL>(AffineMap.lineMap a b) r < (AffineMap.lineMap a' b) r
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>OrderedRing k<VAR>OrderedAddCommGroup E<VAR>Module k E<VAR>OrderedSMul k E<VAR>a b b' : E<VAR>r : k<VAR>hb : b ≤ b'<VAR>hr : 0 ≤ r<GOAL>(AffineMap.lineMap a b) r ≤ (AffineMap.lineMap a b') r
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>OrderedRing k<VAR>OrderedAddCommGroup E<VAR>Module k E<VAR>OrderedSMul k E<VAR>a b b' : E<VAR>r : k<VAR>hb : b < b'<VAR>hr : 0 < r<GOAL>(AffineMap.lineMap a b) r < (AffineMap.lineMap a b') r
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>OrderedRing k<VAR>OrderedAddCommGroup E<VAR>Module k E<VAR>OrderedSMul k E<VAR>a a' b b' : E<VAR>r : k<VAR>ha : a ≤ a'<VAR>hb : b ≤ b'<VAR>h₀ : 0 ≤ r<VAR>h₁ : r ≤ 1<GOAL>(AffineMap.lineMap a b) r ≤ (AffineMap.lineMap a' b') r
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>OrderedRing k<VAR>OrderedAddCommGroup E<VAR>Module k E<VAR>OrderedSMul k E<VAR>a a' b b' : E<VAR>r : k<VAR>ha : a < a'<VAR>hb : b < b'<VAR>h₀ : 0 ≤ r<VAR>h₁ : r ≤ 1<GOAL>(AffineMap.lineMap a b) r < (AffineMap.lineMap a' b') r
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>OrderedRing k<VAR>OrderedAddCommGroup E<VAR>Module k E<VAR>OrderedSMul k E<VAR>a b : E<VAR>r r' : k<VAR>h : r < r'<GOAL>(AffineMap.lineMap a b) r < (AffineMap.lineMap a b) r' ↔ a < b
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>OrderedRing k<VAR>OrderedAddCommGroup E<VAR>Module k E<VAR>OrderedSMul k E<VAR>a b : E<VAR>r : k<VAR>h : 0 < r<GOAL>a < (AffineMap.lineMap a b) r ↔ a < b
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>OrderedRing k<VAR>OrderedAddCommGroup E<VAR>Module k E<VAR>OrderedSMul k E<VAR>a b : E<VAR>r : k<VAR>h : 0 < r<GOAL>(AffineMap.lineMap a b) r < a ↔ b < a
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>OrderedRing k<VAR>OrderedAddCommGroup E<VAR>Module k E<VAR>OrderedSMul k E<VAR>a b : E<VAR>r : k<VAR>h : r < 1<GOAL>(AffineMap.lineMap a b) r < b ↔ a < b
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>OrderedRing k<VAR>OrderedAddCommGroup E<VAR>Module k E<VAR>OrderedSMul k E<VAR>a b : E<VAR>r : k<VAR>h : r < 1<GOAL>b < (AffineMap.lineMap a b) r ↔ b < a
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedRing k<VAR>OrderedAddCommGroup E<VAR>Module k E<VAR>OrderedSMul k E<VAR>Invertible 2<VAR>a a' b b' : E<VAR>ha : a ≤ a'<VAR>hb : b ≤ b'<GOAL>midpoint k a b ≤ midpoint k a' b'
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField k<VAR>OrderedAddCommGroup E<VAR>Module k E<VAR>OrderedSMul k E<VAR>a b : E<VAR>r r' : k<VAR>h : r < r'<GOAL>(AffineMap.lineMap a b) r ≤ (AffineMap.lineMap a b) r' ↔ a ≤ b
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField k<VAR>OrderedAddCommGroup E<VAR>Module k E<VAR>OrderedSMul k E<VAR>a b : E<VAR>r : k<VAR>h : 0 < r<GOAL>a ≤ (AffineMap.lineMap a b) r ↔ a ≤ b
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField k<VAR>OrderedAddCommGroup E<VAR>Module k E<VAR>OrderedSMul k E<VAR>a b : E<GOAL>a ≤ midpoint k a b ↔ a ≤ b
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField k<VAR>OrderedAddCommGroup E<VAR>Module k E<VAR>OrderedSMul k E<VAR>a b : E<VAR>r : k<VAR>h : 0 < r<GOAL>(AffineMap.lineMap a b) r ≤ a ↔ b ≤ a
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField k<VAR>OrderedAddCommGroup E<VAR>Module k E<VAR>OrderedSMul k E<VAR>a b : E<GOAL>midpoint k a b ≤ a ↔ b ≤ a
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField k<VAR>OrderedAddCommGroup E<VAR>Module k E<VAR>OrderedSMul k E<VAR>a b : E<VAR>r : k<VAR>h : r < 1<GOAL>(AffineMap.lineMap a b) r ≤ b ↔ a ≤ b
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField k<VAR>OrderedAddCommGroup E<VAR>Module k E<VAR>OrderedSMul k E<VAR>a b : E<GOAL>midpoint k a b ≤ b ↔ a ≤ b
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField k<VAR>OrderedAddCommGroup E<VAR>Module k E<VAR>OrderedSMul k E<VAR>a b : E<VAR>r : k<VAR>h : r < 1<GOAL>b ≤ (AffineMap.lineMap a b) r ↔ b ≤ a
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField k<VAR>OrderedAddCommGroup E<VAR>Module k E<VAR>OrderedSMul k E<VAR>a b : E<GOAL>b ≤ midpoint k a b ↔ b ≤ a
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField k<VAR>OrderedAddCommGroup E<VAR>Module k E<VAR>OrderedSMul k E<VAR>f : k → E<VAR>a b r : k<VAR>h : 0 < r * (b - a)<GOAL>f ((AffineMap.lineMap a b) r) ≤ (AffineMap.lineMap (f a) (f b)) r ↔ slope f a ((AffineMap.lineMap a b) r) ≤ slope f a b
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField k<VAR>OrderedAddCommGroup E<VAR>Module k E<VAR>OrderedSMul k E<VAR>f : k → E<VAR>a b r : k<VAR>h : 0 < r * (b - a)<GOAL>(AffineMap.lineMap (f a) (f b)) r ≤ f ((AffineMap.lineMap a b) r) ↔ slope f a b ≤ slope f a ((AffineMap.lineMap a b) r)
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField k<VAR>OrderedAddCommGroup E<VAR>Module k E<VAR>OrderedSMul k E<VAR>f : k → E<VAR>a b r : k<VAR>h : 0 < r * (b - a)<GOAL>f ((AffineMap.lineMap a b) r) < (AffineMap.lineMap (f a) (f b)) r ↔ slope f a ((AffineMap.lineMap a b) r) < slope f a b
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField k<VAR>OrderedAddCommGroup E<VAR>Module k E<VAR>OrderedSMul k E<VAR>f : k → E<VAR>a b r : k<VAR>h : 0 < r * (b - a)<GOAL>(AffineMap.lineMap (f a) (f b)) r < f ((AffineMap.lineMap a b) r) ↔ slope f a b < slope f a ((AffineMap.lineMap a b) r)
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField k<VAR>OrderedAddCommGroup E<VAR>Module k E<VAR>OrderedSMul k E<VAR>f : k → E<VAR>a b r : k<VAR>h : 0 < (1 - r) * (b - a)<GOAL>f ((AffineMap.lineMap a b) r) ≤ (AffineMap.lineMap (f a) (f b)) r ↔ slope f a b ≤ slope f ((AffineMap.lineMap a b) r) b
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField k<VAR>OrderedAddCommGroup E<VAR>Module k E<VAR>OrderedSMul k E<VAR>f : k → E<VAR>a b r : k<VAR>h : 0 < (1 - r) * (b - a)<GOAL>(AffineMap.lineMap (f a) (f b)) r ≤ f ((AffineMap.lineMap a b) r) ↔ slope f ((AffineMap.lineMap a b) r) b ≤ slope f a b
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField k<VAR>OrderedAddCommGroup E<VAR>Module k E<VAR>OrderedSMul k E<VAR>f : k → E<VAR>a b r : k<VAR>h : 0 < (1 - r) * (b - a)<GOAL>f ((AffineMap.lineMap a b) r) < (AffineMap.lineMap (f a) (f b)) r ↔ slope f a b < slope f ((AffineMap.lineMap a b) r) b
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField k<VAR>OrderedAddCommGroup E<VAR>Module k E<VAR>OrderedSMul k E<VAR>f : k → E<VAR>a b r : k<VAR>h : 0 < (1 - r) * (b - a)<GOAL>(AffineMap.lineMap (f a) (f b)) r < f ((AffineMap.lineMap a b) r) ↔ slope f ((AffineMap.lineMap a b) r) b < slope f a b