ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>inst✝³¹ : CommRing A<VAR>inst✝³⁰ : CommRing B<VAR>inst✝²⁹ : Algebra A B<VAR>inst✝²⁸ : Field K<VAR>inst✝²⁷ : Field L<VAR>inst✝²⁶ : Algebra A K<VAR>inst✝²⁵ : IsFractionRing A K<VAR>inst✝²⁴ : Algebra B L<VAR>inst✝²³ : Algebra K L<VAR>inst✝²² : Algebra A L<VAR>inst✝²¹ : IsScalarTower A B L<VAR>inst✝²⁰ : IsScalarTower A K L<VAR>inst✝¹⁹ : IsIntegralClosure B A L<VAR>inst✝¹⁸ : FiniteDimensional K L<VAR>Aₘ : Type ?u.512830<VAR>Bₘ : Type ?u.512833<VAR>inst✝¹⁷ : CommRing Aₘ<VAR>inst✝¹⁶ : CommRing Bₘ<VAR>inst✝¹⁵ : Algebra Aₘ Bₘ<VAR>inst✝¹⁴ : Algebra A Aₘ<VAR>inst✝¹³ : Algebra B Bₘ<VAR>inst✝¹² : Algebra A Bₘ<VAR>inst✝¹¹ : IsScalarTower A Aₘ Bₘ<VAR>inst✝¹⁰ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝⁹ : IsLocalization M Aₘ<VAR>inst✝⁸ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝⁷ : IsIntegrallyClosed A<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : IsIntegrallyClosed A<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : IsIntegrallyClosed B<VAR>inst✝² : Module.Finite A B<VAR>inst✝¹ : NoZeroSMulDivisors A B<VAR>inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>x : B<VAR>this : IsIntegralClosure B A (FractionRing B)<GOAL>(algebraMap A K) ((intNorm A B) x) = (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>inst✝³¹ : CommRing A<VAR>inst✝³⁰ : CommRing B<VAR>inst✝²⁹ : Algebra A B<VAR>inst✝²⁸ : Field K<VAR>inst✝²⁷ : Field L<VAR>inst✝²⁶ : Algebra A K<VAR>inst✝²⁵ : IsFractionRing A K<VAR>inst✝²⁴ : Algebra B L<VAR>inst✝²³ : Algebra K L<VAR>inst✝²² : Algebra A L<VAR>inst✝²¹ : IsScalarTower A B L<VAR>inst✝²⁰ : IsScalarTower A K L<VAR>inst✝¹⁹ : IsIntegralClosure B A L<VAR>inst✝¹⁸ : FiniteDimensional K L<VAR>Aₘ : Type ?u.512830<VAR>Bₘ : Type ?u.512833<VAR>inst✝¹⁷ : CommRing Aₘ<VAR>inst✝¹⁶ : CommRing Bₘ<VAR>inst✝¹⁵ : Algebra Aₘ Bₘ<VAR>inst✝¹⁴ : Algebra A Aₘ<VAR>inst✝¹³ : Algebra B Bₘ<VAR>inst✝¹² : Algebra A Bₘ<VAR>inst✝¹¹ : IsScalarTower A Aₘ Bₘ<VAR>inst✝¹⁰ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝⁹ : IsLocalization M Aₘ<VAR>inst✝⁸ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝⁷ : IsIntegrallyClosed A<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : IsIntegrallyClosed A<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : IsIntegrallyClosed B<VAR>inst✝² : Module.Finite A B<VAR>inst✝¹ : NoZeroSMulDivisors A B<VAR>inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>x : B<VAR>this✝ : IsIntegralClosure B A (FractionRing B)<VAR>this : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)<GOAL>(algebraMap A K) ((intNorm A B) x) = (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>inst✝³¹ : CommRing A<VAR>inst✝³⁰ : CommRing B<VAR>inst✝²⁹ : Algebra A B<VAR>inst✝²⁸ : Field K<VAR>inst✝²⁷ : Field L<VAR>inst✝²⁶ : Algebra A K<VAR>inst✝²⁵ : IsFractionRing A K<VAR>inst✝²⁴ : Algebra B L<VAR>inst✝²³ : Algebra K L<VAR>inst✝²² : Algebra A L<VAR>inst✝²¹ : IsScalarTower A B L<VAR>inst✝²⁰ : IsScalarTower A K L<VAR>inst✝¹⁹ : IsIntegralClosure B A L<VAR>inst✝¹⁸ : FiniteDimensional K L<VAR>Aₘ : Type ?u.512830<VAR>Bₘ : Type ?u.512833<VAR>inst✝¹⁷ : CommRing Aₘ<VAR>inst✝¹⁶ : CommRing Bₘ<VAR>inst✝¹⁵ : Algebra Aₘ Bₘ<VAR>inst✝¹⁴ : Algebra A Aₘ<VAR>inst✝¹³ : Algebra B Bₘ<VAR>inst✝¹² : Algebra A Bₘ<VAR>inst✝¹¹ : IsScalarTower A Aₘ Bₘ<VAR>inst✝¹⁰ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝⁹ : IsLocalization M Aₘ<VAR>inst✝⁸ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝⁷ : IsIntegrallyClosed A<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : IsIntegrallyClosed A<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : IsIntegrallyClosed B<VAR>inst✝² : Module.Finite A B<VAR>inst✝¹ : NoZeroSMulDivisors A B<VAR>inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>x : B<VAR>this✝¹ : IsIntegralClosure B A (FractionRing B)<VAR>this✝ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)<VAR>this : FiniteDimensional (FractionRing A) (FractionRing B)<GOAL>(algebraMap A K) ((intNorm A B) x) = (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>inst✝³¹ : CommRing A<VAR>inst✝³⁰ : CommRing B<VAR>inst✝²⁹ : Algebra A B<VAR>inst✝²⁸ : Field K<VAR>inst✝²⁷ : Field L<VAR>inst✝²⁶ : Algebra A K<VAR>inst✝²⁵ : IsFractionRing A K<VAR>inst✝²⁴ : Algebra B L<VAR>inst✝²³ : Algebra K L<VAR>inst✝²² : Algebra A L<VAR>inst✝²¹ : IsScalarTower A B L<VAR>inst✝²⁰ : IsScalarTower A K L<VAR>inst✝¹⁹ : IsIntegralClosure B A L<VAR>inst✝¹⁸ : FiniteDimensional K L<VAR>Aₘ : Type ?u.512830<VAR>Bₘ : Type ?u.512833<VAR>inst✝¹⁷ : CommRing Aₘ<VAR>inst✝¹⁶ : CommRing Bₘ<VAR>inst✝¹⁵ : Algebra Aₘ Bₘ<VAR>inst✝¹⁴ : Algebra A Aₘ<VAR>inst✝¹³ : Algebra B Bₘ<VAR>inst✝¹² : Algebra A Bₘ<VAR>inst✝¹¹ : IsScalarTower A Aₘ Bₘ<VAR>inst✝¹⁰ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝⁹ : IsLocalization M Aₘ<VAR>inst✝⁸ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝⁷ : IsIntegrallyClosed A<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : IsIntegrallyClosed A<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : IsIntegrallyClosed B<VAR>inst✝² : Module.Finite A B<VAR>inst✝¹ : NoZeroSMulDivisors A B<VAR>inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>x : B<VAR>this✝² : IsIntegralClosure B A (FractionRing B)<VAR>this✝¹ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)<VAR>this✝ : FiniteDimensional (FractionRing A) (FractionRing B)<VAR>this : IsFractionRing B L<GOAL>(algebraMap A K) ((intNorm A B) x) = (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>inst✝³¹ : CommRing A<VAR>inst✝³⁰ : CommRing B<VAR>inst✝²⁹ : Algebra A B<VAR>inst✝²⁸ : Field K<VAR>inst✝²⁷ : Field L<VAR>inst✝²⁶ : Algebra A K<VAR>inst✝²⁵ : IsFractionRing A K<VAR>inst✝²⁴ : Algebra B L<VAR>inst✝²³ : Algebra K L<VAR>inst✝²² : Algebra A L<VAR>inst✝²¹ : IsScalarTower A B L<VAR>inst✝²⁰ : IsScalarTower A K L<VAR>inst✝¹⁹ : IsIntegralClosure B A L<VAR>inst✝¹⁸ : FiniteDimensional K L<VAR>Aₘ : Type ?u.512830<VAR>Bₘ : Type ?u.512833<VAR>inst✝¹⁷ : CommRing Aₘ<VAR>inst✝¹⁶ : CommRing Bₘ<VAR>inst✝¹⁵ : Algebra Aₘ Bₘ<VAR>inst✝¹⁴ : Algebra A Aₘ<VAR>inst✝¹³ : Algebra B Bₘ<VAR>inst✝¹² : Algebra A Bₘ<VAR>inst✝¹¹ : IsScalarTower A Aₘ Bₘ<VAR>inst✝¹⁰ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝⁹ : IsLocalization M Aₘ<VAR>inst✝⁸ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝⁷ : IsIntegrallyClosed A<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : IsIntegrallyClosed A<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : IsIntegrallyClosed B<VAR>inst✝² : Module.Finite A B<VAR>inst✝¹ : NoZeroSMulDivisors A B<VAR>inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>x : B<VAR>this✝² : IsIntegralClosure B A (FractionRing B)<VAR>this✝¹ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)<VAR>this✝ : FiniteDimensional (FractionRing A) (FractionRing B)<VAR>this : IsFractionRing B L<GOAL>(FractionRing.algEquiv A K).symm ((algebraMap A K) ((intNorm A B) x)) = (FractionRing.algEquiv A K).symm ((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>inst✝³¹ : CommRing A<VAR>inst✝³⁰ : CommRing B<VAR>inst✝²⁹ : Algebra A B<VAR>inst✝²⁸ : Field K<VAR>inst✝²⁷ : Field L<VAR>inst✝²⁶ : Algebra A K<VAR>inst✝²⁵ : IsFractionRing A K<VAR>inst✝²⁴ : Algebra B L<VAR>inst✝²³ : Algebra K L<VAR>inst✝²² : Algebra A L<VAR>inst✝²¹ : IsScalarTower A B L<VAR>inst✝²⁰ : IsScalarTower A K L<VAR>inst✝¹⁹ : IsIntegralClosure B A L<VAR>inst✝¹⁸ : FiniteDimensional K L<VAR>Aₘ : Type ?u.512830<VAR>Bₘ : Type ?u.512833<VAR>inst✝¹⁷ : CommRing Aₘ<VAR>inst✝¹⁶ : CommRing Bₘ<VAR>inst✝¹⁵ : Algebra Aₘ Bₘ<VAR>inst✝¹⁴ : Algebra A Aₘ<VAR>inst✝¹³ : Algebra B Bₘ<VAR>inst✝¹² : Algebra A Bₘ<VAR>inst✝¹¹ : IsScalarTower A Aₘ Bₘ<VAR>inst✝¹⁰ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝⁹ : IsLocalization M Aₘ<VAR>inst✝⁸ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝⁷ : IsIntegrallyClosed A<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : IsIntegrallyClosed A<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : IsIntegrallyClosed B<VAR>inst✝² : Module.Finite A B<VAR>inst✝¹ : NoZeroSMulDivisors A B<VAR>inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>x : B<VAR>this✝² : IsIntegralClosure B A (FractionRing B)<VAR>this✝¹ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)<VAR>this✝ : FiniteDimensional (FractionRing A) (FractionRing B)<VAR>this : IsFractionRing B L<GOAL>(norm (FractionRing A)) ((algebraMap B (FractionRing B)) x) = (FractionRing.algEquiv A K).symm ((norm K) ((FractionRing.algEquiv B L) ((algebraMap B (FractionRing B)) x)))
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>inst✝³¹ : CommRing A<VAR>inst✝³⁰ : CommRing B<VAR>inst✝²⁹ : Algebra A B<VAR>inst✝²⁸ : Field K<VAR>inst✝²⁷ : Field L<VAR>inst✝²⁶ : Algebra A K<VAR>inst✝²⁵ : IsFractionRing A K<VAR>inst✝²⁴ : Algebra B L<VAR>inst✝²³ : Algebra K L<VAR>inst✝²² : Algebra A L<VAR>inst✝²¹ : IsScalarTower A B L<VAR>inst✝²⁰ : IsScalarTower A K L<VAR>inst✝¹⁹ : IsIntegralClosure B A L<VAR>inst✝¹⁸ : FiniteDimensional K L<VAR>Aₘ : Type ?u.512830<VAR>Bₘ : Type ?u.512833<VAR>inst✝¹⁷ : CommRing Aₘ<VAR>inst✝¹⁶ : CommRing Bₘ<VAR>inst✝¹⁵ : Algebra Aₘ Bₘ<VAR>inst✝¹⁴ : Algebra A Aₘ<VAR>inst✝¹³ : Algebra B Bₘ<VAR>inst✝¹² : Algebra A Bₘ<VAR>inst✝¹¹ : IsScalarTower A Aₘ Bₘ<VAR>inst✝¹⁰ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝⁹ : IsLocalization M Aₘ<VAR>inst✝⁸ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝⁷ : IsIntegrallyClosed A<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : IsIntegrallyClosed A<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : IsIntegrallyClosed B<VAR>inst✝² : Module.Finite A B<VAR>inst✝¹ : NoZeroSMulDivisors A B<VAR>inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>x : B<VAR>this✝² : IsIntegralClosure B A (FractionRing B)<VAR>this✝¹ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)<VAR>this✝ : FiniteDimensional (FractionRing A) (FractionRing B)<VAR>this : IsFractionRing B L<GOAL>(algebraMap K L).comp ↑(FractionRing.algEquiv A K).toRingEquiv = (↑(FractionRing.algEquiv B L).toRingEquiv).comp (algebraMap (FractionRing A) (FractionRing B))
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>inst✝³¹ : CommRing A<VAR>inst✝³⁰ : CommRing B<VAR>inst✝²⁹ : Algebra A B<VAR>inst✝²⁸ : Field K<VAR>inst✝²⁷ : Field L<VAR>inst✝²⁶ : Algebra A K<VAR>inst✝²⁵ : IsFractionRing A K<VAR>inst✝²⁴ : Algebra B L<VAR>inst✝²³ : Algebra K L<VAR>inst✝²² : Algebra A L<VAR>inst✝²¹ : IsScalarTower A B L<VAR>inst✝²⁰ : IsScalarTower A K L<VAR>inst✝¹⁹ : IsIntegralClosure B A L<VAR>inst✝¹⁸ : FiniteDimensional K L<VAR>Aₘ : Type ?u.512830<VAR>Bₘ : Type ?u.512833<VAR>inst✝¹⁷ : CommRing Aₘ<VAR>inst✝¹⁶ : CommRing Bₘ<VAR>inst✝¹⁵ : Algebra Aₘ Bₘ<VAR>inst✝¹⁴ : Algebra A Aₘ<VAR>inst✝¹³ : Algebra B Bₘ<VAR>inst✝¹² : Algebra A Bₘ<VAR>inst✝¹¹ : IsScalarTower A Aₘ Bₘ<VAR>inst✝¹⁰ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝⁹ : IsLocalization M Aₘ<VAR>inst✝⁸ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝⁷ : IsIntegrallyClosed A<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : IsIntegrallyClosed A<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : IsIntegrallyClosed B<VAR>inst✝² : Module.Finite A B<VAR>inst✝¹ : NoZeroSMulDivisors A B<VAR>inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>x : B<VAR>this✝² : IsIntegralClosure B A (FractionRing B)<VAR>this✝¹ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)<VAR>this✝ : FiniteDimensional (FractionRing A) (FractionRing B)<VAR>this : IsFractionRing B L<GOAL>((algebraMap K L).comp ↑(FractionRing.algEquiv A K).toRingEquiv).comp (algebraMap A (FractionRing A)) = ((↑(FractionRing.algEquiv B L).toRingEquiv).comp (algebraMap (FractionRing A) (FractionRing B))).comp (algebraMap A (FractionRing A))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁴ : CommSemiring R<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹¹ : CommRing R₁<VAR>inst✝¹⁰ : AddCommGroup M₁<VAR>inst✝⁹ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : AddCommGroup V<VAR>inst✝⁶ : Module K V<VAR>M'✝ : Type u_7<VAR>M'' : Type u_8<VAR>inst✝⁵ : AddCommMonoid M'✝<VAR>inst✝⁴ : AddCommMonoid M''<VAR>inst✝³ : Module R M'✝<VAR>inst✝² : Module R M''<VAR>B : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>F : BilinForm R M<VAR>M' : Type u_9<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>B' : BilinForm R M'<VAR>f f' : M →ₗ[R] M'<VAR>g g' : M' →ₗ[R] M<VAR>h : B.IsAdjointPair B' f g<VAR>h' : B.IsAdjointPair B' f' g'<VAR>x : M<VAR>y : M'<GOAL>(B' ((f + f') x)) y = (B x) ((g + g') y)
<VAR>y : ℝ<GOAL>0 ^ y * 0 ^ y = 0 ^ y
<VAR>y : ℝ<GOAL>((if 0 < y then 0 else if y = 0 then 1 else ⊤) * if 0 < y then 0 else if y = 0 then 1 else ⊤) = if 0 < y then 0 else if y = 0 then 1 else ⊤
<VAR>y : ℝ<VAR>h✝ : 0 < y<GOAL>0 * 0 = 0
<VAR>y : ℝ<VAR>h✝¹ : ¬0 < y<VAR>h✝ : y = 0<GOAL>1 * 1 = 1
<VAR>y : ℝ<VAR>h✝¹ : ¬0 < y<VAR>h✝ : ¬y = 0<GOAL>⊤ * ⊤ = ⊤
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : Ideal R<VAR>hI : I ≠ 0<GOAL>∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = ↑I
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : Ideal R<VAR>hI : I ≠ 0<GOAL>∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = ↑(∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : Ideal R<VAR>hI : I ≠ 0<GOAL>∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = ∏ᶠ (a : HeightOneSpectrum R), ↑(a.maxPowDividing I)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>inst✝ : DecidableEq ι<VAR>w : ι → k<VAR>p : ι → P<VAR>i : ι<GOAL>((s.erase i).weightedVSubOfPoint p (p i)) w = (s.weightedVSubOfPoint p (p i)) w
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>inst✝ : DecidableEq ι<VAR>w : ι → k<VAR>p : ι → P<VAR>i : ι<GOAL>∑ i_1 ∈ s.erase i, w i_1 • (p i_1 -ᵥ p i) = ∑ i_1 ∈ s, w i_1 • (p i_1 -ᵥ p i)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>inst✝ : DecidableEq ι<VAR>w : ι → k<VAR>p : ι → P<VAR>i : ι<GOAL>w i • (p i -ᵥ p i) = 0
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type v'<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup N<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R N<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Module S N<VAR>inst✝² : IsScalarTower R S N<VAR>p : Submonoid R<VAR>inst✝¹ : IsLocalization p S<VAR>f : M →ₗ[R] N<VAR>inst✝ : IsLocalizedModule p f<VAR>hp : p ≤ R⁰<GOAL>Cardinal.lift.{v, v'} (Module.rank S N) = Cardinal.lift.{v', v} (Module.rank R M)
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type v'<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup N<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R N<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Module S N<VAR>inst✝² : IsScalarTower R S N<VAR>p : Submonoid R<VAR>inst✝¹ : IsLocalization p S<VAR>f : M →ₗ[R] N<VAR>inst✝ : IsLocalizedModule p f<VAR>hp : p ≤ R⁰<VAR>h✝ : Subsingleton R<GOAL>Cardinal.lift.{v, v'} (Module.rank S N) = Cardinal.lift.{v', v} (Module.rank R M)
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type v'<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup N<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R N<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Module S N<VAR>inst✝² : IsScalarTower R S N<VAR>p : Submonoid R<VAR>inst✝¹ : IsLocalization p S<VAR>f : M →ₗ[R] N<VAR>inst✝ : IsLocalizedModule p f<VAR>hp : p ≤ R⁰<VAR>h✝ : Nontrivial R<GOAL>Cardinal.lift.{v, v'} (Module.rank S N) = Cardinal.lift.{v', v} (Module.rank R M)
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type v'<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup N<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R N<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Module S N<VAR>inst✝² : IsScalarTower R S N<VAR>p : Submonoid R<VAR>inst✝¹ : IsLocalization p S<VAR>f : M →ₗ[R] N<VAR>inst✝ : IsLocalizedModule p f<VAR>hp : p ≤ R⁰<VAR>h✝ : Nontrivial R<VAR>this : Nontrivial S<GOAL>Cardinal.lift.{v, v'} (Module.rank S N) = Cardinal.lift.{v', v} (Module.rank R M)
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type v'<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup N<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R N<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Module S N<VAR>inst✝² : IsScalarTower R S N<VAR>p : Submonoid R<VAR>inst✝¹ : IsLocalization p S<VAR>f : M →ₗ[R] N<VAR>inst✝ : IsLocalizedModule p f<VAR>hp : p ≤ R⁰<VAR>h✝ : Nontrivial R<VAR>this : Nontrivial S<GOAL>Cardinal.lift.{v, v'} (Module.rank S N) ≤ Cardinal.lift.{v', v} (Module.rank R M)
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type v'<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup N<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R N<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Module S N<VAR>inst✝² : IsScalarTower R S N<VAR>p : Submonoid R<VAR>inst✝¹ : IsLocalization p S<VAR>f : M →ₗ[R] N<VAR>inst✝ : IsLocalizedModule p f<VAR>hp : p ≤ R⁰<VAR>h✝ : Nontrivial R<VAR>this : Nontrivial S<GOAL>Cardinal.lift.{v', v} (Module.rank R M) ≤ Cardinal.lift.{v, v'} (Module.rank S N)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k l : ℕ<VAR>inst✝¹ : CommRing R<VAR>ζ✝ : Rˣ<VAR>h✝ : IsPrimitiveRoot ζ✝ k<VAR>inst✝ : IsDomain R<VAR>ζ : R<VAR>n : ℕ<VAR>h : IsPrimitiveRoot ζ n<VAR>a : R<VAR>ha : a ≠ 0<GOAL>(nthRoots n a).Nodup
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k l : ℕ<VAR>inst✝¹ : CommRing R<VAR>ζ✝ : Rˣ<VAR>h✝ : IsPrimitiveRoot ζ✝ k<VAR>inst✝ : IsDomain R<VAR>ζ a : R<VAR>ha : a ≠ 0<VAR>h : IsPrimitiveRoot ζ 0<GOAL>(nthRoots 0 a).Nodup
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k l : ℕ<VAR>inst✝¹ : CommRing R<VAR>ζ✝ : Rˣ<VAR>h✝ : IsPrimitiveRoot ζ✝ k<VAR>inst✝ : IsDomain R<VAR>ζ : R<VAR>n : ℕ<VAR>h : IsPrimitiveRoot ζ n<VAR>a : R<VAR>ha : a ≠ 0<VAR>hn : n > 0<GOAL>(nthRoots n a).Nodup
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : CommRing α<VAR>A B : Matrix n n α<VAR>inst✝² : Fintype m<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : CommRing α<VAR>M : Matrix m m α<VAR>h : IsUnit M<VAR>N : Matrix m m α<GOAL>(M * N * M⁻¹).det = N.det
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>h : ∀ x ∈ s, f x = f₁ x<VAR>p : TangentBundle I M<VAR>hp : p.proj ∈ s<VAR>hs : UniqueMDiffWithinAt I s p.proj<GOAL>HEq (tangentMapWithin I I' f s p).snd (tangentMapWithin I I' f₁ s p).snd
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f : Filter α<VAR>inst✝ : f.NeBot<VAR>p : Prop<VAR>q : α → Prop<GOAL>(∃ᶠ (x : α) in f, p → q x) ↔ p → ∃ᶠ (x : α) in f, q x
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝³ : Field R<VAR>p q : R[X]<VAR>inst✝² : CommRing S<VAR>inst✝¹ : IsDomain S<VAR>inst✝ : Algebra R S<VAR>ι : Type u_1<VAR>f : ι → R[X]<VAR>s : Finset ι<VAR>h : s.prod f ≠ 0<GOAL>(s.prod f).rootSet S = ⋃ i ∈ s, (f i).rootSet S
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝¹ : Preorder ι<VAR>inst✝ : IsMarkovKernel κ<VAR>s : ι → Set Ω<VAR>hsm : ∀ (n : ι), MeasurableSet (s n)<VAR>hs : iIndepSet s κ μ<VAR>i : ι<GOAL>Indep (generateFrom {s i}) (generateFrom {t | ∃ j < i, s j = t}) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝¹ : Preorder ι<VAR>inst✝ : IsMarkovKernel κ<VAR>s : ι → Set Ω<VAR>hsm : ∀ (n : ι), MeasurableSet (s n)<VAR>hs : iIndepSet s κ μ<VAR>i : ι<GOAL>{s i} = {t | ∃ n ∈ {i}, s n = t}
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>hμm : SigmaFinite (μ.trim hm)<VAR>f : α → F'<VAR>hf : AEStronglyMeasurable' m f μ<VAR>hfi : Integrable f μ<GOAL>μ[f|m] =ᶠ[ae μ] f
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>hμm : SigmaFinite (μ.trim hm)<VAR>f : α → F'<VAR>hf : AEStronglyMeasurable' m f μ<VAR>hfi : Integrable f μ<GOAL>μ[AEStronglyMeasurable'.mk f hf|m] =ᶠ[ae μ] AEStronglyMeasurable'.mk f hf
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => x + a) ⁻¹' Icc b c = Icc (b - a) (c - a)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B' I J D X : Set α<VAR>e f : α<VAR>hI : M.Indep I<VAR>hne : I.Nonempty<GOAL>M.RkPos
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B✝ B' I J D X : Set α<VAR>e f : α<VAR>hI : M.Indep I<VAR>hne : I.Nonempty<VAR>B : Set α<VAR>hB : M.Base B<VAR>hIB : I ⊆ B<GOAL>M.RkPos
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>inst✝⁶ : MulOneClass M<VAR>inst✝⁵ : MulOneClass N<VAR>inst✝⁴ : FunLike F M N<VAR>inst✝³ : FunLike F G H<VAR>inst✝² : DivInvMonoid G<VAR>inst✝¹ : DivInvMonoid H<VAR>inst✝ : MonoidHomClass F G H<VAR>f : F<VAR>hf : ∀ (x : G), f x⁻¹ = (f x)⁻¹<VAR>g : ι → G<VAR>n : ℤ<VAR>x✝ : ι<GOAL>(⇑f ∘ (g ^ n)) x✝ = (⇑f ∘ g ^ n) x✝
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a✝ : α<VAR>n✝ n a : ℕ<GOAL>⌈↑n⌉₊ ≤ a ↔ n ≤ a