ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝²⁰ : CommRing A<VAR>inst✝¹⁹ : Field K<VAR>inst✝¹⁸ : CommRing B<VAR>inst✝¹⁷ : Field L<VAR>inst✝¹⁶ : Algebra A K<VAR>inst✝¹⁵ : Algebra B L<VAR>inst✝¹⁴ : Algebra A B<VAR>inst✝¹³ : Algebra K L<VAR>inst✝¹² : Algebra A L<VAR>inst✝¹¹ : IsScalarTower A K L<VAR>inst✝¹⁰ : IsScalarTower A B L<VAR>inst✝⁹ : IsDomain A<VAR>inst✝⁸ : IsFractionRing A K<VAR>inst✝⁷ : IsIntegralClosure B A L<VAR>inst✝⁶ : IsFractionRing B L<VAR>inst✝⁵ : FiniteDimensional K L<VAR>inst✝⁴ : Algebra.IsSeparable K L<VAR>inst✝³ : IsDomain B<VAR>inst✝² : IsIntegrallyClosed A<VAR>I : Submodule B L<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>b : Basis ι K L<VAR>hb : ∀ (i : ι), IsIntegral A (b i)<VAR>a x : L<VAR>ha : a ∈ I<VAR>hx : x ∈ Iᵛ<VAR>hinv : IsUnit (traceMatrix K ⇑b).det<VAR>H : (traceMatrix K ⇑b *ᵥ (traceMatrix K ⇑b).cramer fun i => (Algebra.trace K L) (x * a * b i)) = (traceMatrix K ⇑b).det • fun i => (Algebra.trace K L) (x * a * b i)<GOAL>IsIntegral A (discr K ⇑b • a * x)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝²⁰ : CommRing A<VAR>inst✝¹⁹ : Field K<VAR>inst✝¹⁸ : CommRing B<VAR>inst✝¹⁷ : Field L<VAR>inst✝¹⁶ : Algebra A K<VAR>inst✝¹⁵ : Algebra B L<VAR>inst✝¹⁴ : Algebra A B<VAR>inst✝¹³ : Algebra K L<VAR>inst✝¹² : Algebra A L<VAR>inst✝¹¹ : IsScalarTower A K L<VAR>inst✝¹⁰ : IsScalarTower A B L<VAR>inst✝⁹ : IsDomain A<VAR>inst✝⁸ : IsFractionRing A K<VAR>inst✝⁷ : IsIntegralClosure B A L<VAR>inst✝⁶ : IsFractionRing B L<VAR>inst✝⁵ : FiniteDimensional K L<VAR>inst✝⁴ : Algebra.IsSeparable K L<VAR>inst✝³ : IsDomain B<VAR>inst✝² : IsIntegrallyClosed A<VAR>I : Submodule B L<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>b : Basis ι K L<VAR>hb : ∀ (i : ι), IsIntegral A (b i)<VAR>a x : L<VAR>ha : a ∈ I<VAR>hx : x ∈ Iᵛ<VAR>hinv : IsUnit (traceMatrix K ⇑b).det<VAR>H : (traceMatrix K ⇑b *ᵥ (traceMatrix K ⇑b).cramer fun i => (Algebra.trace K L) (x * a * b i)) = (traceMatrix K ⇑b).det • fun i => (Algebra.trace K L) (x * a * b i)<VAR>this : Function.Injective (traceMatrix K ⇑b).mulVec<GOAL>IsIntegral A (discr K ⇑b • a * x)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝²⁰ : CommRing A<VAR>inst✝¹⁹ : Field K<VAR>inst✝¹⁸ : CommRing B<VAR>inst✝¹⁷ : Field L<VAR>inst✝¹⁶ : Algebra A K<VAR>inst✝¹⁵ : Algebra B L<VAR>inst✝¹⁴ : Algebra A B<VAR>inst✝¹³ : Algebra K L<VAR>inst✝¹² : Algebra A L<VAR>inst✝¹¹ : IsScalarTower A K L<VAR>inst✝¹⁰ : IsScalarTower A B L<VAR>inst✝⁹ : IsDomain A<VAR>inst✝⁸ : IsFractionRing A K<VAR>inst✝⁷ : IsIntegralClosure B A L<VAR>inst✝⁶ : IsFractionRing B L<VAR>inst✝⁵ : FiniteDimensional K L<VAR>inst✝⁴ : Algebra.IsSeparable K L<VAR>inst✝³ : IsDomain B<VAR>inst✝² : IsIntegrallyClosed A<VAR>I : Submodule B L<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>b : Basis ι K L<VAR>hb : ∀ (i : ι), IsIntegral A (b i)<VAR>a x : L<VAR>ha : a ∈ I<VAR>hx : x ∈ Iᵛ<VAR>hinv : IsUnit (traceMatrix K ⇑b).det<VAR>H : ((traceMatrix K ⇑b).cramer fun i => (Algebra.trace K L) (x * a * b i)) = (traceMatrix K ⇑b).det • b.equivFun (x * a)<VAR>this : Function.Injective (traceMatrix K ⇑b).mulVec<GOAL>IsIntegral A (discr K ⇑b • a * x)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝²⁰ : CommRing A<VAR>inst✝¹⁹ : Field K<VAR>inst✝¹⁸ : CommRing B<VAR>inst✝¹⁷ : Field L<VAR>inst✝¹⁶ : Algebra A K<VAR>inst✝¹⁵ : Algebra B L<VAR>inst✝¹⁴ : Algebra A B<VAR>inst✝¹³ : Algebra K L<VAR>inst✝¹² : Algebra A L<VAR>inst✝¹¹ : IsScalarTower A K L<VAR>inst✝¹⁰ : IsScalarTower A B L<VAR>inst✝⁹ : IsDomain A<VAR>inst✝⁸ : IsFractionRing A K<VAR>inst✝⁷ : IsIntegralClosure B A L<VAR>inst✝⁶ : IsFractionRing B L<VAR>inst✝⁵ : FiniteDimensional K L<VAR>inst✝⁴ : Algebra.IsSeparable K L<VAR>inst✝³ : IsDomain B<VAR>inst✝² : IsIntegrallyClosed A<VAR>I : Submodule B L<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>b : Basis ι K L<VAR>hb : ∀ (i : ι), IsIntegral A (b i)<VAR>a x : L<VAR>ha : a ∈ I<VAR>hx : x ∈ Iᵛ<VAR>hinv : IsUnit (traceMatrix K ⇑b).det<VAR>H : ((traceMatrix K ⇑b).cramer fun i => (Algebra.trace K L) (x * a * b i)) = (traceMatrix K ⇑b).det • b.equivFun (x * a)<VAR>this : Function.Injective (traceMatrix K ⇑b).mulVec<GOAL>IsIntegral A (∑ i : ι, b.equivFun (discr K ⇑b • a * x) i • b i)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝²⁰ : CommRing A<VAR>inst✝¹⁹ : Field K<VAR>inst✝¹⁸ : CommRing B<VAR>inst✝¹⁷ : Field L<VAR>inst✝¹⁶ : Algebra A K<VAR>inst✝¹⁵ : Algebra B L<VAR>inst✝¹⁴ : Algebra A B<VAR>inst✝¹³ : Algebra K L<VAR>inst✝¹² : Algebra A L<VAR>inst✝¹¹ : IsScalarTower A K L<VAR>inst✝¹⁰ : IsScalarTower A B L<VAR>inst✝⁹ : IsDomain A<VAR>inst✝⁸ : IsFractionRing A K<VAR>inst✝⁷ : IsIntegralClosure B A L<VAR>inst✝⁶ : IsFractionRing B L<VAR>inst✝⁵ : FiniteDimensional K L<VAR>inst✝⁴ : Algebra.IsSeparable K L<VAR>inst✝³ : IsDomain B<VAR>inst✝² : IsIntegrallyClosed A<VAR>I : Submodule B L<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>b : Basis ι K L<VAR>hb : ∀ (i : ι), IsIntegral A (b i)<VAR>a x : L<VAR>ha : a ∈ I<VAR>hx : x ∈ Iᵛ<VAR>hinv : IsUnit (traceMatrix K ⇑b).det<VAR>H : ((traceMatrix K ⇑b).cramer fun i => (Algebra.trace K L) (x * a * b i)) = (traceMatrix K ⇑b).det • b.equivFun (x * a)<VAR>this : Function.Injective (traceMatrix K ⇑b).mulVec<GOAL>∀ x_1 ∈ Finset.univ, IsIntegral A (b.equivFun (discr K ⇑b • a * x) x_1 • b x_1)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝²⁰ : CommRing A<VAR>inst✝¹⁹ : Field K<VAR>inst✝¹⁸ : CommRing B<VAR>inst✝¹⁷ : Field L<VAR>inst✝¹⁶ : Algebra A K<VAR>inst✝¹⁵ : Algebra B L<VAR>inst✝¹⁴ : Algebra A B<VAR>inst✝¹³ : Algebra K L<VAR>inst✝¹² : Algebra A L<VAR>inst✝¹¹ : IsScalarTower A K L<VAR>inst✝¹⁰ : IsScalarTower A B L<VAR>inst✝⁹ : IsDomain A<VAR>inst✝⁸ : IsFractionRing A K<VAR>inst✝⁷ : IsIntegralClosure B A L<VAR>inst✝⁶ : IsFractionRing B L<VAR>inst✝⁵ : FiniteDimensional K L<VAR>inst✝⁴ : Algebra.IsSeparable K L<VAR>inst✝³ : IsDomain B<VAR>inst✝² : IsIntegrallyClosed A<VAR>I : Submodule B L<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>b : Basis ι K L<VAR>hb : ∀ (i : ι), IsIntegral A (b i)<VAR>a x : L<VAR>ha : a ∈ I<VAR>hx : x ∈ Iᵛ<VAR>hinv : IsUnit (traceMatrix K ⇑b).det<VAR>H : ((traceMatrix K ⇑b).cramer fun i => (Algebra.trace K L) (x * a * b i)) = (traceMatrix K ⇑b).det • b.equivFun (x * a)<VAR>this : Function.Injective (traceMatrix K ⇑b).mulVec<VAR>i : ι<VAR>a✝ : i ∈ Finset.univ<GOAL>IsIntegral A (b.equivFun (discr K ⇑b • a * x) i • b i)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝²⁰ : CommRing A<VAR>inst✝¹⁹ : Field K<VAR>inst✝¹⁸ : CommRing B<VAR>inst✝¹⁷ : Field L<VAR>inst✝¹⁶ : Algebra A K<VAR>inst✝¹⁵ : Algebra B L<VAR>inst✝¹⁴ : Algebra A B<VAR>inst✝¹³ : Algebra K L<VAR>inst✝¹² : Algebra A L<VAR>inst✝¹¹ : IsScalarTower A K L<VAR>inst✝¹⁰ : IsScalarTower A B L<VAR>inst✝⁹ : IsDomain A<VAR>inst✝⁸ : IsFractionRing A K<VAR>inst✝⁷ : IsIntegralClosure B A L<VAR>inst✝⁶ : IsFractionRing B L<VAR>inst✝⁵ : FiniteDimensional K L<VAR>inst✝⁴ : Algebra.IsSeparable K L<VAR>inst✝³ : IsDomain B<VAR>inst✝² : IsIntegrallyClosed A<VAR>I : Submodule B L<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>b : Basis ι K L<VAR>hb : ∀ (i : ι), IsIntegral A (b i)<VAR>a x : L<VAR>ha : a ∈ I<VAR>hx : x ∈ Iᵛ<VAR>hinv : IsUnit (traceMatrix K ⇑b).det<VAR>H : ((traceMatrix K ⇑b).cramer fun i => (Algebra.trace K L) (x * a * b i)) = (traceMatrix K ⇑b).det • b.equivFun (x * a)<VAR>this : Function.Injective (traceMatrix K ⇑b).mulVec<VAR>i : ι<VAR>a✝ : i ∈ Finset.univ<GOAL>IsIntegral A ((algebraMap K L) ((traceMatrix K ⇑b).cramer (fun i => (Algebra.trace K L) (x * a * b i)) i) * b i)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝²⁰ : CommRing A<VAR>inst✝¹⁹ : Field K<VAR>inst✝¹⁸ : CommRing B<VAR>inst✝¹⁷ : Field L<VAR>inst✝¹⁶ : Algebra A K<VAR>inst✝¹⁵ : Algebra B L<VAR>inst✝¹⁴ : Algebra A B<VAR>inst✝¹³ : Algebra K L<VAR>inst✝¹² : Algebra A L<VAR>inst✝¹¹ : IsScalarTower A K L<VAR>inst✝¹⁰ : IsScalarTower A B L<VAR>inst✝⁹ : IsDomain A<VAR>inst✝⁸ : IsFractionRing A K<VAR>inst✝⁷ : IsIntegralClosure B A L<VAR>inst✝⁶ : IsFractionRing B L<VAR>inst✝⁵ : FiniteDimensional K L<VAR>inst✝⁴ : Algebra.IsSeparable K L<VAR>inst✝³ : IsDomain B<VAR>inst✝² : IsIntegrallyClosed A<VAR>I : Submodule B L<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>b : Basis ι K L<VAR>hb : ∀ (i : ι), IsIntegral A (b i)<VAR>a x : L<VAR>ha : a ∈ I<VAR>hx : x ∈ Iᵛ<VAR>hinv : IsUnit (traceMatrix K ⇑b).det<VAR>H : ((traceMatrix K ⇑b).cramer fun i => (Algebra.trace K L) (x * a * b i)) = (traceMatrix K ⇑b).det • b.equivFun (x * a)<VAR>this : Function.Injective (traceMatrix K ⇑b).mulVec<VAR>i : ι<VAR>a✝ : i ∈ Finset.univ<GOAL>(algebraMap A L).IsIntegralElem ((algebraMap K L) ((traceMatrix K ⇑b).cramer (fun i => (Algebra.trace K L) (x * a * b i)) i))
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝²⁰ : CommRing A<VAR>inst✝¹⁹ : Field K<VAR>inst✝¹⁸ : CommRing B<VAR>inst✝¹⁷ : Field L<VAR>inst✝¹⁶ : Algebra A K<VAR>inst✝¹⁵ : Algebra B L<VAR>inst✝¹⁴ : Algebra A B<VAR>inst✝¹³ : Algebra K L<VAR>inst✝¹² : Algebra A L<VAR>inst✝¹¹ : IsScalarTower A K L<VAR>inst✝¹⁰ : IsScalarTower A B L<VAR>inst✝⁹ : IsDomain A<VAR>inst✝⁸ : IsFractionRing A K<VAR>inst✝⁷ : IsIntegralClosure B A L<VAR>inst✝⁶ : IsFractionRing B L<VAR>inst✝⁵ : FiniteDimensional K L<VAR>inst✝⁴ : Algebra.IsSeparable K L<VAR>inst✝³ : IsDomain B<VAR>inst✝² : IsIntegrallyClosed A<VAR>I : Submodule B L<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>b : Basis ι K L<VAR>hb : ∀ (i : ι), IsIntegral A (b i)<VAR>a x : L<VAR>ha : a ∈ I<VAR>hx : x ∈ Iᵛ<VAR>hinv : IsUnit (traceMatrix K ⇑b).det<VAR>H : ((traceMatrix K ⇑b).cramer fun i => (Algebra.trace K L) (x * a * b i)) = (traceMatrix K ⇑b).det • b.equivFun (x * a)<VAR>this : Function.Injective (traceMatrix K ⇑b).mulVec<VAR>i : ι<VAR>a✝ : i ∈ Finset.univ<GOAL>IsIntegral A ((traceMatrix K ⇑b).cramer (fun i => (Algebra.trace K L) (x * a * b i)) i)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝²⁰ : CommRing A<VAR>inst✝¹⁹ : Field K<VAR>inst✝¹⁸ : CommRing B<VAR>inst✝¹⁷ : Field L<VAR>inst✝¹⁶ : Algebra A K<VAR>inst✝¹⁵ : Algebra B L<VAR>inst✝¹⁴ : Algebra A B<VAR>inst✝¹³ : Algebra K L<VAR>inst✝¹² : Algebra A L<VAR>inst✝¹¹ : IsScalarTower A K L<VAR>inst✝¹⁰ : IsScalarTower A B L<VAR>inst✝⁹ : IsDomain A<VAR>inst✝⁸ : IsFractionRing A K<VAR>inst✝⁷ : IsIntegralClosure B A L<VAR>inst✝⁶ : IsFractionRing B L<VAR>inst✝⁵ : FiniteDimensional K L<VAR>inst✝⁴ : Algebra.IsSeparable K L<VAR>inst✝³ : IsDomain B<VAR>inst✝² : IsIntegrallyClosed A<VAR>I : Submodule B L<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>b : Basis ι K L<VAR>hb : ∀ (i : ι), IsIntegral A (b i)<VAR>a x : L<VAR>ha : a ∈ I<VAR>hx : x ∈ Iᵛ<VAR>hinv : IsUnit (traceMatrix K ⇑b).det<VAR>H : ((traceMatrix K ⇑b).cramer fun i => (Algebra.trace K L) (x * a * b i)) = (traceMatrix K ⇑b).det • b.equivFun (x * a)<VAR>this : Function.Injective (traceMatrix K ⇑b).mulVec<VAR>i : ι<VAR>a✝ : i ∈ Finset.univ<GOAL>IsIntegral A ((traceMatrix K ⇑b).updateColumn i fun i => (Algebra.trace K L) (x * a * b i)).det
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝²⁰ : CommRing A<VAR>inst✝¹⁹ : Field K<VAR>inst✝¹⁸ : CommRing B<VAR>inst✝¹⁷ : Field L<VAR>inst✝¹⁶ : Algebra A K<VAR>inst✝¹⁵ : Algebra B L<VAR>inst✝¹⁴ : Algebra A B<VAR>inst✝¹³ : Algebra K L<VAR>inst✝¹² : Algebra A L<VAR>inst✝¹¹ : IsScalarTower A K L<VAR>inst✝¹⁰ : IsScalarTower A B L<VAR>inst✝⁹ : IsDomain A<VAR>inst✝⁸ : IsFractionRing A K<VAR>inst✝⁷ : IsIntegralClosure B A L<VAR>inst✝⁶ : IsFractionRing B L<VAR>inst✝⁵ : FiniteDimensional K L<VAR>inst✝⁴ : Algebra.IsSeparable K L<VAR>inst✝³ : IsDomain B<VAR>inst✝² : IsIntegrallyClosed A<VAR>I : Submodule B L<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>b : Basis ι K L<VAR>hb : ∀ (i : ι), IsIntegral A (b i)<VAR>a x : L<VAR>ha : a ∈ I<VAR>hx : x ∈ Iᵛ<VAR>hinv : IsUnit (traceMatrix K ⇑b).det<VAR>H : ((traceMatrix K ⇑b).cramer fun i => (Algebra.trace K L) (x * a * b i)) = (traceMatrix K ⇑b).det • b.equivFun (x * a)<VAR>this : Function.Injective (traceMatrix K ⇑b).mulVec<VAR>i : ι<VAR>a✝ : i ∈ Finset.univ<GOAL>∀ (i_1 j : ι), IsIntegral A ((traceMatrix K ⇑b).updateColumn i (fun i => (Algebra.trace K L) (x * a * b i)) i_1 j)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝²⁰ : CommRing A<VAR>inst✝¹⁹ : Field K<VAR>inst✝¹⁸ : CommRing B<VAR>inst✝¹⁷ : Field L<VAR>inst✝¹⁶ : Algebra A K<VAR>inst✝¹⁵ : Algebra B L<VAR>inst✝¹⁴ : Algebra A B<VAR>inst✝¹³ : Algebra K L<VAR>inst✝¹² : Algebra A L<VAR>inst✝¹¹ : IsScalarTower A K L<VAR>inst✝¹⁰ : IsScalarTower A B L<VAR>inst✝⁹ : IsDomain A<VAR>inst✝⁸ : IsFractionRing A K<VAR>inst✝⁷ : IsIntegralClosure B A L<VAR>inst✝⁶ : IsFractionRing B L<VAR>inst✝⁵ : FiniteDimensional K L<VAR>inst✝⁴ : Algebra.IsSeparable K L<VAR>inst✝³ : IsDomain B<VAR>inst✝² : IsIntegrallyClosed A<VAR>I : Submodule B L<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>b : Basis ι K L<VAR>hb : ∀ (i : ι), IsIntegral A (b i)<VAR>a x : L<VAR>ha : a ∈ I<VAR>hx : x ∈ Iᵛ<VAR>hinv : IsUnit (traceMatrix K ⇑b).det<VAR>H : ((traceMatrix K ⇑b).cramer fun i => (Algebra.trace K L) (x * a * b i)) = (traceMatrix K ⇑b).det • b.equivFun (x * a)<VAR>this : Function.Injective (traceMatrix K ⇑b).mulVec<VAR>i : ι<VAR>a✝ : i ∈ Finset.univ<VAR>j k : ι<GOAL>IsIntegral A ((traceMatrix K ⇑b).updateColumn i (fun i => (Algebra.trace K L) (x * a * b i)) j k)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝²⁰ : CommRing A<VAR>inst✝¹⁹ : Field K<VAR>inst✝¹⁸ : CommRing B<VAR>inst✝¹⁷ : Field L<VAR>inst✝¹⁶ : Algebra A K<VAR>inst✝¹⁵ : Algebra B L<VAR>inst✝¹⁴ : Algebra A B<VAR>inst✝¹³ : Algebra K L<VAR>inst✝¹² : Algebra A L<VAR>inst✝¹¹ : IsScalarTower A K L<VAR>inst✝¹⁰ : IsScalarTower A B L<VAR>inst✝⁹ : IsDomain A<VAR>inst✝⁸ : IsFractionRing A K<VAR>inst✝⁷ : IsIntegralClosure B A L<VAR>inst✝⁶ : IsFractionRing B L<VAR>inst✝⁵ : FiniteDimensional K L<VAR>inst✝⁴ : Algebra.IsSeparable K L<VAR>inst✝³ : IsDomain B<VAR>inst✝² : IsIntegrallyClosed A<VAR>I : Submodule B L<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>b : Basis ι K L<VAR>hb : ∀ (i : ι), IsIntegral A (b i)<VAR>a x : L<VAR>ha : a ∈ I<VAR>hx : x ∈ Iᵛ<VAR>hinv : IsUnit (traceMatrix K ⇑b).det<VAR>H : ((traceMatrix K ⇑b).cramer fun i => (Algebra.trace K L) (x * a * b i)) = (traceMatrix K ⇑b).det • b.equivFun (x * a)<VAR>this : Function.Injective (traceMatrix K ⇑b).mulVec<VAR>i : ι<VAR>a✝ : i ∈ Finset.univ<VAR>j k : ι<GOAL>IsIntegral A (if k = i then (Algebra.trace K L) (x * a * b j) else traceMatrix K (⇑b) j k)
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>G : Type u_3<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>f : ι → 𝕜 → G<VAR>g : 𝕜 → G<VAR>f' : ι → 𝕜 → G<VAR>g' : 𝕜 → G<VAR>x : 𝕜<VAR>inst✝ : l.NeBot<VAR>hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)<VAR>hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasDerivAt (f n.1) (f' n.1 n.2) n.2<VAR>hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))<VAR>F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)<VAR>G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)<GOAL>HasDerivAt g (g' x) x
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>G : Type u_3<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>f : ι → 𝕜 → G<VAR>g : 𝕜 → G<VAR>f' : ι → 𝕜 → G<VAR>g' : 𝕜 → G<VAR>x : 𝕜<VAR>inst✝ : l.NeBot<VAR>hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)<VAR>hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))<VAR>F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)<VAR>G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)<VAR>hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (ContinuousLinearMap.smulRight 1 (f' n.1 n.2)) n.2<GOAL>HasFDerivAt g (ContinuousLinearMap.smulRight 1 (g' x)) x
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>G : Type u_3<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>f : ι → 𝕜 → G<VAR>g : 𝕜 → G<VAR>f' : ι → 𝕜 → G<VAR>g' : 𝕜 → G<VAR>x : 𝕜<VAR>inst✝ : l.NeBot<VAR>hf'✝ : TendstoUniformlyOnFilter f' g' l (𝓝 x)<VAR>hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))<VAR>F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)<VAR>G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)<VAR>hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (ContinuousLinearMap.smulRight 1 (f' n.1 n.2)) n.2<VAR>hf' : TendstoUniformlyOnFilter F' G' l (𝓝 x)<GOAL>HasFDerivAt g (ContinuousLinearMap.smulRight 1 (g' x)) x
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>f : ι → Y<VAR>g : κ → Z<VAR>hf : DenseRange f<VAR>hg : DenseRange g<GOAL>DenseRange (Prod.map f g)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>a : K<GOAL>mixedEmbedding.norm ((mixedEmbedding K) a) = 0 ↔ (mixedEmbedding K) a = 0
<VAR>α : Type u<VAR>β : Type v<VAR>M✝ N✝ M : Matroid α<VAR>N : Matroid β<VAR>I : Set (α ⊕ β)<GOAL>(M.sum N).Indep I ↔ M.Indep (Sum.inl ⁻¹' I) ∧ N.Indep (Sum.inr ⁻¹' I)
<VAR>α : Type u<VAR>β : Type v<VAR>M✝ N✝ M : Matroid α<VAR>N : Matroid β<VAR>I : Set (α ⊕ β)<GOAL>M.Indep ((fun a => a.down) '' (Sigma.mk false ⁻¹' ((fun a => (Equiv.sumEquivSigmaBool (ULift.{v, u} α) (ULift.{u, v} β)) a) '' ((fun a => Sum.map (⇑Equiv.ulift.symm) (⇑Equiv.ulift.symm) a) '' I)))) ∧ N.Indep ((fun a => a.down) '' (Sigma.mk true ⁻¹' ((fun a => (Equiv.sumEquivSigmaBool (ULift.{v, u} α) (ULift.{u, v} β)) a) '' ((fun a => Sum.map (⇑Equiv.ulift.symm) (⇑Equiv.ulift.symm) a) '' I)))) ↔ M.Indep (Sum.inl ⁻¹' I) ∧ N.Indep (Sum.inr ⁻¹' I)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<GOAL>wittMul p 0 = X (0, 0) * X (1, 0)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<GOAL>(map (Int.castRingHom ℚ)) (wittMul p 0) = (map (Int.castRingHom ℚ)) (X (0, 0) * X (1, 0))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : BooleanRing α<VAR>inst✝¹ : BooleanRing β<VAR>inst✝ : BooleanRing γ<VAR>a b : α<GOAL>a * (a + b + a * b) = a
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝¹⁰ : Category.{u_6, u_1} C<VAR>inst✝⁹ : Category.{u_7, u_2} D<VAR>inst✝⁸ : Category.{?u.89019, u_3} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁷ : AddMonoid A<VAR>inst✝⁶ : AddCommMonoid B<VAR>inst✝⁵ : HasShift C A<VAR>inst✝⁴ : HasShift D A<VAR>inst✝³ : HasShift E A<VAR>inst✝² : HasShift C B<VAR>inst✝¹ : HasShift D B<VAR>inst✝ : F.CommShift A<VAR>X : C<VAR>a b : A<VAR>h : a + b = 0<GOAL>F.map ((shiftFunctorCompIsoId C a b h).inv.app X) = (shiftFunctorCompIsoId D a b h).inv.app (F.obj X) ≫ (shiftFunctor D b).map ((F.commShiftIso a).inv.app X) ≫ (F.commShiftIso b).inv.app ((shiftFunctor C a).obj X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝¹⁰ : Category.{u_6, u_1} C<VAR>inst✝⁹ : Category.{u_7, u_2} D<VAR>inst✝⁸ : Category.{?u.89019, u_3} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁷ : AddMonoid A<VAR>inst✝⁶ : AddCommMonoid B<VAR>inst✝⁵ : HasShift C A<VAR>inst✝⁴ : HasShift D A<VAR>inst✝³ : HasShift E A<VAR>inst✝² : HasShift C B<VAR>inst✝¹ : HasShift D B<VAR>inst✝ : F.CommShift A<VAR>X : C<VAR>a b : A<VAR>h : a + b = 0<GOAL>𝟙 (F.obj ((shiftFunctor C a ⋙ shiftFunctor C b).obj X)) = ((F.commShiftIso b).hom.app ((shiftFunctor C a).obj X) ≫ (shiftFunctor D b).map ((F.commShiftIso a).hom.app X) ≫ (shiftFunctorCompIsoId D a b h).hom.app (F.obj X)) ≫ (shiftFunctorCompIsoId D a b h).inv.app (F.obj X) ≫ (shiftFunctor D b).map ((F.commShiftIso a).inv.app X) ≫ (F.commShiftIso b).inv.app ((shiftFunctor C a).obj X)
<VAR>α : Type u_1<VAR>inst✝⁶ : DecidableEq α<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁵ : MulZeroOneClass R<VAR>inst✝⁴ : DecidableEq R<VAR>inst✝³ : Nontrivial R<VAR>inst✝² : MulZeroOneClass S<VAR>inst✝¹ : DecidableEq S<VAR>inst✝ : Nontrivial S<VAR>f : R →*₀ S<VAR>hf : Function.Injective ⇑f<VAR>x y : WithTop R<GOAL>{ toFun := map ⇑f, map_zero' := ⋯ }.toFun (x * y) = { toFun := map ⇑f, map_zero' := ⋯ }.toFun x * { toFun := map ⇑f, map_zero' := ⋯ }.toFun y
<VAR>α : Type u_1<VAR>inst✝⁶ : DecidableEq α<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁵ : MulZeroOneClass R<VAR>inst✝⁴ : DecidableEq R<VAR>inst✝³ : Nontrivial R<VAR>inst✝² : MulZeroOneClass S<VAR>inst✝¹ : DecidableEq S<VAR>inst✝ : Nontrivial S<VAR>f : R →*₀ S<VAR>hf : Function.Injective ⇑f<VAR>x y : WithTop R<VAR>this : ∀ (z : WithTop R), map (⇑f) z = 0 ↔ z = 0<GOAL>{ toFun := map ⇑f, map_zero' := ⋯ }.toFun (x * y) = { toFun := map ⇑f, map_zero' := ⋯ }.toFun x * { toFun := map ⇑f, map_zero' := ⋯ }.toFun y
<VAR>α : Type u_1<VAR>inst✝⁶ : DecidableEq α<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁵ : MulZeroOneClass R<VAR>inst✝⁴ : DecidableEq R<VAR>inst✝³ : Nontrivial R<VAR>inst✝² : MulZeroOneClass S<VAR>inst✝¹ : DecidableEq S<VAR>inst✝ : Nontrivial S<VAR>f : R →*₀ S<VAR>hf : Function.Injective ⇑f<VAR>y : WithTop R<VAR>this : ∀ (z : WithTop R), map (⇑f) z = 0 ↔ z = 0<GOAL>{ toFun := map ⇑f, map_zero' := ⋯ }.toFun (0 * y) = { toFun := map ⇑f, map_zero' := ⋯ }.toFun 0 * { toFun := map ⇑f, map_zero' := ⋯ }.toFun y
<VAR>α : Type u_1<VAR>inst✝⁶ : DecidableEq α<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁵ : MulZeroOneClass R<VAR>inst✝⁴ : DecidableEq R<VAR>inst✝³ : Nontrivial R<VAR>inst✝² : MulZeroOneClass S<VAR>inst✝¹ : DecidableEq S<VAR>inst✝ : Nontrivial S<VAR>f : R →*₀ S<VAR>hf : Function.Injective ⇑f<VAR>x y : WithTop R<VAR>this : ∀ (z : WithTop R), map (⇑f) z = 0 ↔ z = 0<VAR>hx : x ≠ 0<GOAL>{ toFun := map ⇑f, map_zero' := ⋯ }.toFun (x * y) = { toFun := map ⇑f, map_zero' := ⋯ }.toFun x * { toFun := map ⇑f, map_zero' := ⋯ }.toFun y
<VAR>α : Type u_1<VAR>inst✝⁶ : DecidableEq α<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁵ : MulZeroOneClass R<VAR>inst✝⁴ : DecidableEq R<VAR>inst✝³ : Nontrivial R<VAR>inst✝² : MulZeroOneClass S<VAR>inst✝¹ : DecidableEq S<VAR>inst✝ : Nontrivial S<VAR>f : R →*₀ S<VAR>hf : Function.Injective ⇑f<VAR>x : WithTop R<VAR>this : ∀ (z : WithTop R), map (⇑f) z = 0 ↔ z = 0<VAR>hx : x ≠ 0<GOAL>{ toFun := map ⇑f, map_zero' := ⋯ }.toFun (x * 0) = { toFun := map ⇑f, map_zero' := ⋯ }.toFun x * { toFun := map ⇑f, map_zero' := ⋯ }.toFun 0
<VAR>α : Type u_1<VAR>inst✝⁶ : DecidableEq α<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁵ : MulZeroOneClass R<VAR>inst✝⁴ : DecidableEq R<VAR>inst✝³ : Nontrivial R<VAR>inst✝² : MulZeroOneClass S<VAR>inst✝¹ : DecidableEq S<VAR>inst✝ : Nontrivial S<VAR>f : R →*₀ S<VAR>hf : Function.Injective ⇑f<VAR>x y : WithTop R<VAR>this : ∀ (z : WithTop R), map (⇑f) z = 0 ↔ z = 0<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>{ toFun := map ⇑f, map_zero' := ⋯ }.toFun (x * y) = { toFun := map ⇑f, map_zero' := ⋯ }.toFun x * { toFun := map ⇑f, map_zero' := ⋯ }.toFun y
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁵ : Ring α<VAR>inst✝⁴ : LinearOrder α<VAR>a b : α<VAR>inst✝³ : PosMulStrictMono α<VAR>inst✝² : MulPosStrictMono α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>a * b ≤ 0 ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁵ : Ring α<VAR>inst✝⁴ : LinearOrder α<VAR>a b : α<VAR>inst✝³ : PosMulStrictMono α<VAR>inst✝² : MulPosStrictMono α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>(0 < -a → 0 ≤ b) ∧ (0 < b → 0 ≤ -a) ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t✝ : Set α<VAR>i : ι<VAR>p'✝ : ι' → Prop<VAR>s'✝ : ι' → Set α<VAR>i' : ι'<VAR>hl : l.HasBasis p s<VAR>p' : ι → Prop<VAR>s' : ι → Set α<VAR>hp : ∀ (i : ι), p i ↔ p' i<VAR>hs : ∀ (i : ι), p i → s i = s' i<VAR>t : Set α<GOAL>t ∈ l ↔ ∃ i, p' i ∧ s' i ⊆ t