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_5<VAR>Bₘ : Type u_6<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>inst✝⁶ : IsDomain Aₘ<VAR>inst✝⁵ : IsIntegrallyClosed Aₘ<VAR>inst✝⁴ : IsDomain Bₘ<VAR>inst✝³ : IsIntegrallyClosed Bₘ<VAR>inst✝² : NoZeroSMulDivisors Aₘ Bₘ<VAR>inst✝¹ : Module.Finite Aₘ Bₘ<VAR>inst✝ : Algebra.IsSeparable (FractionRing Aₘ) (FractionRing Bₘ)<VAR>x : B<VAR>hM : M ≤ A⁰<GOAL>(algebraMap A Aₘ) ((intNorm A B) x) = (intNorm 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>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_5<VAR>Bₘ : Type u_6<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>inst✝⁶ : IsDomain Aₘ<VAR>inst✝⁵ : IsIntegrallyClosed Aₘ<VAR>inst✝⁴ : IsDomain Bₘ<VAR>inst✝³ : IsIntegrallyClosed Bₘ<VAR>inst✝² : NoZeroSMulDivisors Aₘ Bₘ<VAR>inst✝¹ : Module.Finite Aₘ Bₘ<VAR>inst✝ : Algebra.IsSeparable (FractionRing Aₘ) (FractionRing Bₘ)<VAR>x : B<VAR>hM : M ≤ A⁰<VAR>K : Type u_1 := FractionRing A<VAR>L : Type u_4 := FractionRing B<VAR>this : IsIntegralClosure B A L<GOAL>(algebraMap A Aₘ) ((intNorm A B) x) = (intNorm 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>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_5<VAR>Bₘ : Type u_6<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>inst✝⁶ : IsDomain Aₘ<VAR>inst✝⁵ : IsIntegrallyClosed Aₘ<VAR>inst✝⁴ : IsDomain Bₘ<VAR>inst✝³ : IsIntegrallyClosed Bₘ<VAR>inst✝² : NoZeroSMulDivisors Aₘ Bₘ<VAR>inst✝¹ : Module.Finite Aₘ Bₘ<VAR>inst✝ : Algebra.IsSeparable (FractionRing Aₘ) (FractionRing Bₘ)<VAR>x : B<VAR>hM : M ≤ A⁰<VAR>K : Type u_1 := FractionRing A<VAR>L : Type u_4 := FractionRing B<VAR>this✝ : IsIntegralClosure B A L<VAR>this : IsLocalization (algebraMapSubmonoid B A⁰) L<GOAL>(algebraMap A Aₘ) ((intNorm A B) x) = (intNorm 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>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_5<VAR>Bₘ : Type u_6<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>inst✝⁶ : IsDomain Aₘ<VAR>inst✝⁵ : IsIntegrallyClosed Aₘ<VAR>inst✝⁴ : IsDomain Bₘ<VAR>inst✝³ : IsIntegrallyClosed Bₘ<VAR>inst✝² : NoZeroSMulDivisors Aₘ Bₘ<VAR>inst✝¹ : Module.Finite Aₘ Bₘ<VAR>inst✝ : Algebra.IsSeparable (FractionRing Aₘ) (FractionRing Bₘ)<VAR>x : B<VAR>hM : M ≤ A⁰<VAR>K : Type u_1 := FractionRing A<VAR>L : Type u_4 := FractionRing B<VAR>this✝¹ : IsIntegralClosure B A L<VAR>this✝ : IsLocalization (algebraMapSubmonoid B A⁰) L<VAR>f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM<VAR>this : Algebra Aₘ K := f.toAlgebra<GOAL>(algebraMap A Aₘ) ((intNorm A B) x) = (intNorm 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>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_5<VAR>Bₘ : Type u_6<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>inst✝⁶ : IsDomain Aₘ<VAR>inst✝⁵ : IsIntegrallyClosed Aₘ<VAR>inst✝⁴ : IsDomain Bₘ<VAR>inst✝³ : IsIntegrallyClosed Bₘ<VAR>inst✝² : NoZeroSMulDivisors Aₘ Bₘ<VAR>inst✝¹ : Module.Finite Aₘ Bₘ<VAR>inst✝ : Algebra.IsSeparable (FractionRing Aₘ) (FractionRing Bₘ)<VAR>x : B<VAR>hM : M ≤ A⁰<VAR>K : Type u_1 := FractionRing A<VAR>L : Type u_4 := FractionRing B<VAR>this✝² : IsIntegralClosure B A L<VAR>this✝¹ : IsLocalization (algebraMapSubmonoid B A⁰) L<VAR>f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM<VAR>this✝ : Algebra Aₘ K := f.toAlgebra<VAR>this : IsScalarTower A Aₘ K<GOAL>(algebraMap A Aₘ) ((intNorm A B) x) = (intNorm 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>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_5<VAR>Bₘ : Type u_6<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>inst✝⁶ : IsDomain Aₘ<VAR>inst✝⁵ : IsIntegrallyClosed Aₘ<VAR>inst✝⁴ : IsDomain Bₘ<VAR>inst✝³ : IsIntegrallyClosed Bₘ<VAR>inst✝² : NoZeroSMulDivisors Aₘ Bₘ<VAR>inst✝¹ : Module.Finite Aₘ Bₘ<VAR>inst✝ : Algebra.IsSeparable (FractionRing Aₘ) (FractionRing Bₘ)<VAR>x : B<VAR>hM : M ≤ A⁰<VAR>K : Type u_1 := FractionRing A<VAR>L : Type u_4 := FractionRing B<VAR>this✝³ : IsIntegralClosure B A L<VAR>this✝² : IsLocalization (algebraMapSubmonoid B A⁰) L<VAR>f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM<VAR>this✝¹ : Algebra Aₘ K := f.toAlgebra<VAR>this✝ : IsScalarTower A Aₘ K<VAR>this : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K<GOAL>(algebraMap A Aₘ) ((intNorm A B) x) = (intNorm 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>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_5<VAR>Bₘ : Type u_6<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>inst✝⁶ : IsDomain Aₘ<VAR>inst✝⁵ : IsIntegrallyClosed Aₘ<VAR>inst✝⁴ : IsDomain Bₘ<VAR>inst✝³ : IsIntegrallyClosed Bₘ<VAR>inst✝² : NoZeroSMulDivisors Aₘ Bₘ<VAR>inst✝¹ : Module.Finite Aₘ Bₘ<VAR>inst✝ : Algebra.IsSeparable (FractionRing Aₘ) (FractionRing Bₘ)<VAR>x : B<VAR>hM : M ≤ A⁰<VAR>K : Type u_1 := FractionRing A<VAR>L : Type u_4 := FractionRing B<VAR>this✝³ : IsIntegralClosure B A L<VAR>this✝² : IsLocalization (algebraMapSubmonoid B A⁰) L<VAR>f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM<VAR>this✝¹ : Algebra Aₘ K := f.toAlgebra<VAR>this✝ : IsScalarTower A Aₘ K<VAR>this : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K<VAR>g : Bₘ →+* L := IsLocalization.map L (RingHom.id B) ⋯<GOAL>(algebraMap A Aₘ) ((intNorm A B) x) = (intNorm 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>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_5<VAR>Bₘ : Type u_6<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>inst✝⁶ : IsDomain Aₘ<VAR>inst✝⁵ : IsIntegrallyClosed Aₘ<VAR>inst✝⁴ : IsDomain Bₘ<VAR>inst✝³ : IsIntegrallyClosed Bₘ<VAR>inst✝² : NoZeroSMulDivisors Aₘ Bₘ<VAR>inst✝¹ : Module.Finite Aₘ Bₘ<VAR>inst✝ : Algebra.IsSeparable (FractionRing Aₘ) (FractionRing Bₘ)<VAR>x : B<VAR>hM : M ≤ A⁰<VAR>K : Type u_1 := FractionRing A<VAR>L : Type u_4 := FractionRing B<VAR>this✝⁴ : IsIntegralClosure B A L<VAR>this✝³ : IsLocalization (algebraMapSubmonoid B A⁰) L<VAR>f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM<VAR>this✝² : Algebra Aₘ K := f.toAlgebra<VAR>this✝¹ : IsScalarTower A Aₘ K<VAR>this✝ : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K<VAR>g : Bₘ →+* L := IsLocalization.map L (RingHom.id B) ⋯<VAR>this : Algebra Bₘ L := g.toAlgebra<GOAL>(algebraMap A Aₘ) ((intNorm A B) x) = (intNorm 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>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_5<VAR>Bₘ : Type u_6<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>inst✝⁶ : IsDomain Aₘ<VAR>inst✝⁵ : IsIntegrallyClosed Aₘ<VAR>inst✝⁴ : IsDomain Bₘ<VAR>inst✝³ : IsIntegrallyClosed Bₘ<VAR>inst✝² : NoZeroSMulDivisors Aₘ Bₘ<VAR>inst✝¹ : Module.Finite Aₘ Bₘ<VAR>inst✝ : Algebra.IsSeparable (FractionRing Aₘ) (FractionRing Bₘ)<VAR>x : B<VAR>hM : M ≤ A⁰<VAR>K : Type u_1 := FractionRing A<VAR>L : Type u_4 := FractionRing B<VAR>this✝⁵ : IsIntegralClosure B A L<VAR>this✝⁴ : IsLocalization (algebraMapSubmonoid B A⁰) L<VAR>f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM<VAR>this✝³ : Algebra Aₘ K := f.toAlgebra<VAR>this✝² : IsScalarTower A Aₘ K<VAR>this✝¹ : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K<VAR>g : Bₘ →+* L := IsLocalization.map L (RingHom.id B) ⋯<VAR>this✝ : Algebra Bₘ L := g.toAlgebra<VAR>this : IsScalarTower B Bₘ L<GOAL>(algebraMap A Aₘ) ((intNorm A B) x) = (intNorm 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>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_5<VAR>Bₘ : Type u_6<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>inst✝⁶ : IsDomain Aₘ<VAR>inst✝⁵ : IsIntegrallyClosed Aₘ<VAR>inst✝⁴ : IsDomain Bₘ<VAR>inst✝³ : IsIntegrallyClosed Bₘ<VAR>inst✝² : NoZeroSMulDivisors Aₘ Bₘ<VAR>inst✝¹ : Module.Finite Aₘ Bₘ<VAR>inst✝ : Algebra.IsSeparable (FractionRing Aₘ) (FractionRing Bₘ)<VAR>x : B<VAR>hM : M ≤ A⁰<VAR>K : Type u_1 := FractionRing A<VAR>L : Type u_4 := FractionRing B<VAR>this✝⁶ : IsIntegralClosure B A L<VAR>this✝⁵ : IsLocalization (algebraMapSubmonoid B A⁰) L<VAR>f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM<VAR>this✝⁴ : Algebra Aₘ K := f.toAlgebra<VAR>this✝³ : IsScalarTower A Aₘ K<VAR>this✝² : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K<VAR>g : Bₘ →+* L := IsLocalization.map L (RingHom.id B) ⋯<VAR>this✝¹ : Algebra Bₘ L := g.toAlgebra<VAR>this✝ : IsScalarTower B Bₘ L<VAR>this : Algebra Aₘ L := ((algebraMap K L).comp f).toAlgebra<GOAL>(algebraMap A Aₘ) ((intNorm A B) x) = (intNorm 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>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_5<VAR>Bₘ : Type u_6<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>inst✝⁶ : IsDomain Aₘ<VAR>inst✝⁵ : IsIntegrallyClosed Aₘ<VAR>inst✝⁴ : IsDomain Bₘ<VAR>inst✝³ : IsIntegrallyClosed Bₘ<VAR>inst✝² : NoZeroSMulDivisors Aₘ Bₘ<VAR>inst✝¹ : Module.Finite Aₘ Bₘ<VAR>inst✝ : Algebra.IsSeparable (FractionRing Aₘ) (FractionRing Bₘ)<VAR>x : B<VAR>hM : M ≤ A⁰<VAR>K : Type u_1 := FractionRing A<VAR>L : Type u_4 := FractionRing B<VAR>this✝⁷ : IsIntegralClosure B A L<VAR>this✝⁶ : IsLocalization (algebraMapSubmonoid B A⁰) L<VAR>f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM<VAR>this✝⁵ : Algebra Aₘ K := f.toAlgebra<VAR>this✝⁴ : IsScalarTower A Aₘ K<VAR>this✝³ : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K<VAR>g : Bₘ →+* L := IsLocalization.map L (RingHom.id B) ⋯<VAR>this✝² : Algebra Bₘ L := g.toAlgebra<VAR>this✝¹ : IsScalarTower B Bₘ L<VAR>this✝ : Algebra Aₘ L := ((algebraMap K L).comp f).toAlgebra<VAR>this : IsScalarTower Aₘ K L<GOAL>(algebraMap A Aₘ) ((intNorm A B) x) = (intNorm 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>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_5<VAR>Bₘ : Type u_6<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>inst✝⁶ : IsDomain Aₘ<VAR>inst✝⁵ : IsIntegrallyClosed Aₘ<VAR>inst✝⁴ : IsDomain Bₘ<VAR>inst✝³ : IsIntegrallyClosed Bₘ<VAR>inst✝² : NoZeroSMulDivisors Aₘ Bₘ<VAR>inst✝¹ : Module.Finite Aₘ Bₘ<VAR>inst✝ : Algebra.IsSeparable (FractionRing Aₘ) (FractionRing Bₘ)<VAR>x : B<VAR>hM : M ≤ A⁰<VAR>K : Type u_1 := FractionRing A<VAR>L : Type u_4 := FractionRing B<VAR>this✝⁸ : IsIntegralClosure B A L<VAR>this✝⁷ : IsLocalization (algebraMapSubmonoid B A⁰) L<VAR>f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM<VAR>this✝⁶ : Algebra Aₘ K := f.toAlgebra<VAR>this✝⁵ : IsScalarTower A Aₘ K<VAR>this✝⁴ : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K<VAR>g : Bₘ →+* L := IsLocalization.map L (RingHom.id B) ⋯<VAR>this✝³ : Algebra Bₘ L := g.toAlgebra<VAR>this✝² : IsScalarTower B Bₘ L<VAR>this✝¹ : Algebra Aₘ L := ((algebraMap K L).comp f).toAlgebra<VAR>this✝ : IsScalarTower Aₘ K L<VAR>this : IsScalarTower Aₘ Bₘ L<GOAL>(algebraMap A Aₘ) ((intNorm A B) x) = (intNorm Aₘ Bₘ) ((algebraMap B Bₘ) x)