internlm/Lean-Github huggingface dataset:
Theorem: Ideal.NoZeroSMulDivisors_of_isLocalization
Proof state before:
case intro.intro.intro.intro.intro.intro
R✝ : Type u_1
inst✝²⁹ : CommRing R✝
S✝ : Type u_2
inst✝²⁸ : CommRing S✝
inst✝²⁷ : Algebra R✝ S✝
inst✝²⁶ : IsIntegrallyClosed R✝
inst✝²⁵ : IsDomain R✝
inst✝²⁴ : IsDomain S✝
inst✝²³ : NoZeroSMulDivisors R✝ S✝
hRS : Module.Finite R✝ S✝
inst✝²² : IsIntegrallyClosed S✝
inst✝²¹ : IsSeparable (FractionRing R✝) (FractionRing S✝)
inst✝²⁰ : IsDomain R✝
inst✝¹⁹ : IsDomain S✝
inst✝¹⁸ : IsDedekindDomain R✝
inst✝¹⁷ : IsDedekindDomain S✝
inst✝¹⁶ : Module.Finite R✝ S✝
inst✝¹⁵ : Module.Free R✝ S✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : R
s : ↥M
a : R
ha : a ∈ ↑M
H : (algebraMap R S) a * (algebraMap R S) x = 0
⊢ ∃ a ∈ M, a * x = 0
Tactic:
simp only [← _root_.map_mul,
  (injective_iff_map_eq_zero' _).mp (NoZeroSMulDivisors.algebraMap_injective R S)] at H
Proof state after:
case intro.intro.intro.intro.intro.intro
R✝ : Type u_1
inst✝²⁹ : CommRing R✝
S✝ : Type u_2
inst✝²⁸ : CommRing S✝
inst✝²⁷ : Algebra R✝ S✝
inst✝²⁶ : IsIntegrallyClosed R✝
inst✝²⁵ : IsDomain R✝
inst✝²⁴ : IsDomain S✝
inst✝²³ : NoZeroSMulDivisors R✝ S✝
hRS : Module.Finite R✝ S✝
inst✝²² : IsIntegrallyClosed S✝
inst✝²¹ : IsSeparable (FractionRing R✝) (FractionRing S✝)
inst✝²⁰ : IsDomain R✝
inst✝¹⁹ : IsDomain S✝
inst✝¹⁸ : IsDedekindDomain R✝
inst✝¹⁷ : IsDedekindDomain S✝
inst✝¹⁶ : Module.Finite R✝ S✝
inst✝¹⁵ : Module.Free R✝ S✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : R
s : ↥M
a : R
ha : a ∈ ↑M
H : a * x = 0
⊢ ∃ a ∈ M, a * x = 0
Theorem: Ideal.NoZeroSMulDivisors_of_isLocalization
Proof state before:
case intro.intro.intro.intro.intro.intro
R✝ : Type u_1
inst✝²⁹ : CommRing R✝
S✝ : Type u_2
inst✝²⁸ : CommRing S✝
inst✝²⁷ : Algebra R✝ S✝
inst✝²⁶ : IsIntegrallyClosed R✝
inst✝²⁵ : IsDomain R✝
inst✝²⁴ : IsDomain S✝
inst✝²³ : NoZeroSMulDivisors R✝ S✝
hRS : Module.Finite R✝ S✝
inst✝²² : IsIntegrallyClosed S✝
inst✝²¹ : IsSeparable (FractionRing R✝) (FractionRing S✝)
inst✝²⁰ : IsDomain R✝
inst✝¹⁹ : IsDomain S✝
inst✝¹⁸ : IsDedekindDomain R✝
inst✝¹⁷ : IsDedekindDomain S✝
inst✝¹⁶ : Module.Finite R✝ S✝
inst✝¹⁵ : Module.Free R✝ S✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : R
s : ↥M
a : R
ha : a ∈ ↑M
H : a * x = 0
⊢ ∃ a ∈ M, a * x = 0
Tactic:
refine ⟨a, ha, H⟩
Proof state after:
no goals
Theorem: Ideal.NoZeroSMulDivisors_of_isLocalization
Proof state before:
R✝ : Type u_1
inst✝²⁹ : CommRing R✝
S✝ : Type u_2
inst✝²⁸ : CommRing S✝
inst✝²⁷ : Algebra R✝ S✝
inst✝²⁶ : IsIntegrallyClosed R✝
inst✝²⁵ : IsDomain R✝
inst✝²⁴ : IsDomain S✝
inst✝²³ : NoZeroSMulDivisors R✝ S✝
hRS : Module.Finite R✝ S✝
inst✝²² : IsIntegrallyClosed S✝
inst✝²¹ : IsSeparable (FractionRing R✝) (FractionRing S✝)
inst✝²⁰ : IsDomain R✝
inst✝¹⁹ : IsDomain S✝
inst✝¹⁸ : IsDedekindDomain R✝
inst✝¹⁷ : IsDedekindDomain S✝
inst✝¹⁶ : Module.Finite R✝ S✝
inst✝¹⁵ : Module.Free R✝ S✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this : IsDomain Sₚ
⊢ algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
Tactic:
apply IsLocalization.ringHom_ext M
Proof state after:
case h
R✝ : Type u_1
inst✝²⁹ : CommRing R✝
S✝ : Type u_2
inst✝²⁸ : CommRing S✝
inst✝²⁷ : Algebra R✝ S✝
inst✝²⁶ : IsIntegrallyClosed R✝
inst✝²⁵ : IsDomain R✝
inst✝²⁴ : IsDomain S✝
inst✝²³ : NoZeroSMulDivisors R✝ S✝
hRS : Module.Finite R✝ S✝
inst✝²² : IsIntegrallyClosed S✝
inst✝²¹ : IsSeparable (FractionRing R✝) (FractionRing S✝)
inst✝²⁰ : IsDomain R✝
inst✝¹⁹ : IsDomain S✝
inst✝¹⁸ : IsDedekindDomain R✝
inst✝¹⁷ : IsDedekindDomain S✝
inst✝¹⁶ : Module.Finite R✝ S✝
inst✝¹⁵ : Module.Free R✝ S✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this : IsDomain Sₚ
⊢ (algebraMap Rₚ Sₚ).comp (algebraMap R Rₚ) = (IsLocalization.map Sₚ (algebraMap R S) ⋯).comp (algebraMap R Rₚ)
Theorem: Ideal.NoZeroSMulDivisors_of_isLocalization
Proof state before:
case h
R✝ : Type u_1
inst✝²⁹ : CommRing R✝
S✝ : Type u_2
inst✝²⁸ : CommRing S✝
inst✝²⁷ : Algebra R✝ S✝
inst✝²⁶ : IsIntegrallyClosed R✝
inst✝²⁵ : IsDomain R✝
inst✝²⁴ : IsDomain S✝
inst✝²³ : NoZeroSMulDivisors R✝ S✝
hRS : Module.Finite R✝ S✝
inst✝²² : IsIntegrallyClosed S✝
inst✝²¹ : IsSeparable (FractionRing R✝) (FractionRing S✝)
inst✝²⁰ : IsDomain R✝
inst✝¹⁹ : IsDomain S✝
inst✝¹⁸ : IsDedekindDomain R✝
inst✝¹⁷ : IsDedekindDomain S✝
inst✝¹⁶ : Module.Finite R✝ S✝
inst✝¹⁵ : Module.Free R✝ S✝
R : Type u_3
S : Type u_4
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing Rₚ
inst✝¹¹ : CommRing Sₚ
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : Algebra R Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra Rₚ Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝³ : IsLocalization M Rₚ
inst✝² : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsDomain S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this : IsDomain Sₚ
⊢ (algebraMap Rₚ Sₚ).comp (algebraMap R Rₚ) = (IsLocalization.map Sₚ (algebraMap R S) ⋯).comp (algebraMap R Rₚ)
Tactic:
simp only [IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]
Proof state after:
no goals
Theorem: Ideal.IsLocalization.AtPrime.PID_of_dedekind_domain
Proof state before:
R : Type u_1
inst✝²⁰ : CommRing R
S : Type u_2
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
inst✝¹⁷ : IsIntegrallyClosed R
inst✝¹⁶ : IsDomain R
inst✝¹⁵ : IsDomain S
inst✝¹⁴ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝¹³ : IsIntegrallyClosed S
inst✝¹² : IsSeparable (FractionRing R) (FractionRing S)
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : IsDedekindDomain R
inst✝⁸ : IsDedekindDomain S
inst✝⁷ : Module.Finite R S
inst✝⁶ : Module.Free R S
A : Type u_4
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
P : Ideal A
pP : P.IsPrime
Aₘ : Type u_3
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
⊢ IsPrincipalIdealRing Aₘ
Tactic:
letI : IsNoetherianRing Aₘ :=
  IsLocalization.isNoetherianRing P.primeCompl _ IsDedekindRing.toIsNoetherian
Proof state after:
R : Type u_1
inst✝²⁰ : CommRing R
S : Type u_2
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
inst✝¹⁷ : IsIntegrallyClosed R
inst✝¹⁶ : IsDomain R
inst✝¹⁵ : IsDomain S
inst✝¹⁴ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝¹³ : IsIntegrallyClosed S
inst✝¹² : IsSeparable (FractionRing R) (FractionRing S)
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : IsDedekindDomain R
inst✝⁸ : IsDedekindDomain S
inst✝⁷ : Module.Finite R S
inst✝⁶ : Module.Free R S
A : Type u_4
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
P : Ideal A
pP : P.IsPrime
Aₘ : Type u_3
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
this : IsNoetherianRing Aₘ := IsLocalization.isNoetherianRing P.primeCompl Aₘ IsDedekindRing.toIsNoetherian
⊢ IsPrincipalIdealRing Aₘ
Theorem: Ideal.IsLocalization.AtPrime.PID_of_dedekind_domain
Proof state before:
R : Type u_1
inst✝²⁰ : CommRing R
S : Type u_2
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
inst✝¹⁷ : IsIntegrallyClosed R
inst✝¹⁶ : IsDomain R
inst✝¹⁵ : IsDomain S
inst✝¹⁴ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝¹³ : IsIntegrallyClosed S
inst✝¹² : IsSeparable (FractionRing R) (FractionRing S)
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : IsDedekindDomain R
inst✝⁸ : IsDedekindDomain S
inst✝⁷ : Module.Finite R S
inst✝⁶ : Module.Free R S
A : Type u_4
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
P : Ideal A
pP : P.IsPrime
Aₘ : Type u_3
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
this : IsNoetherianRing Aₘ := IsLocalization.isNoetherianRing P.primeCompl Aₘ IsDedekindRing.toIsNoetherian
⊢ IsPrincipalIdealRing Aₘ
Tactic:
letI : LocalRing Aₘ := IsLocalization.AtPrime.localRing Aₘ P
Proof state after:
R : Type u_1
inst✝²⁰ : CommRing R
S : Type u_2
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
inst✝¹⁷ : IsIntegrallyClosed R
inst✝¹⁶ : IsDomain R
inst✝¹⁵ : IsDomain S
inst✝¹⁴ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝¹³ : IsIntegrallyClosed S
inst✝¹² : IsSeparable (FractionRing R) (FractionRing S)
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : IsDedekindDomain R
inst✝⁸ : IsDedekindDomain S
inst✝⁷ : Module.Finite R S
inst✝⁶ : Module.Free R S
A : Type u_4
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
P : Ideal A
pP : P.IsPrime
Aₘ : Type u_3
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
this✝ : IsNoetherianRing Aₘ := IsLocalization.isNoetherianRing P.primeCompl Aₘ IsDedekindRing.toIsNoetherian
this : LocalRing Aₘ := IsLocalization.AtPrime.localRing Aₘ P
⊢ IsPrincipalIdealRing Aₘ
Theorem: Ideal.IsLocalization.AtPrime.PID_of_dedekind_domain
Proof state before:
R : Type u_1
inst✝²⁰ : CommRing R
S : Type u_2
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
inst✝¹⁷ : IsIntegrallyClosed R
inst✝¹⁶ : IsDomain R
inst✝¹⁵ : IsDomain S
inst✝¹⁴ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝¹³ : IsIntegrallyClosed S
inst✝¹² : IsSeparable (FractionRing R) (FractionRing S)
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : IsDedekindDomain R
inst✝⁸ : IsDedekindDomain S
inst✝⁷ : Module.Finite R S
inst✝⁶ : Module.Free R S
A : Type u_4
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
P : Ideal A
pP : P.IsPrime
Aₘ : Type u_3
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization.AtPrime Aₘ P
this✝ : IsNoetherianRing Aₘ := IsLocalization.isNoetherianRing P.primeCompl Aₘ IsDedekindRing.toIsNoetherian
this : LocalRing Aₘ := IsLocalization.AtPrime.localRing Aₘ P
⊢ IsPrincipalIdealRing Aₘ
Tactic:
exact ((tfae_of_isNoetherianRing_of_localRing_of_isDomain Aₘ).out 2 0).mp
  (IsLocalization.AtPrime.isDedekindDomain A P _)
Proof state after:
no goals
Theorem: Ideal.spanIntNorm_mul
Proof state before:
R : Type u_1
inst✝¹⁴ : CommRing R
S : Type u_2
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
inst✝¹¹ : IsIntegrallyClosed R
inst✝¹⁰ : IsDomain R
inst✝⁹ : IsDomain S
inst✝⁸ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁷ : IsIntegrallyClosed S
inst✝⁶ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁵ : IsDomain R
inst✝⁴ : IsDomain S
inst✝³ : IsDedekindDomain R
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite R S
inst✝ : Module.Free R S
I J : Ideal S
⊢ spanIntNorm R (I * J) = spanIntNorm R I * spanIntNorm R J
Tactic:
nontriviality R
Proof state after:
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
⊢ spanIntNorm R (I * J) = spanIntNorm R I * spanIntNorm R J
Theorem: Ideal.spanIntNorm_mul
Proof state before:
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
⊢ spanIntNorm R (I * J) = spanIntNorm R I * spanIntNorm R J
Tactic:
cases subsingleton_or_nontrivial S
Proof state after:
case inl
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Subsingleton S
⊢ spanIntNorm R (I * J) = spanIntNorm R I * spanIntNorm R J

case inr
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
⊢ spanIntNorm R (I * J) = spanIntNorm R I * spanIntNorm R J
Theorem: Ideal.spanIntNorm_mul
Proof state before:
case inr
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
⊢ spanIntNorm R (I * J) = spanIntNorm R I * spanIntNorm R J
Tactic:
refine eq_of_localization_maximal ?_
Proof state after:
case inr
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
⊢ ∀ (P : Ideal R) (x : P.IsMaximal),
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
      map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)
Theorem: Ideal.spanIntNorm_mul
Proof state before:
case inr
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
⊢ ∀ (P : Ideal R) (x : P.IsMaximal),
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
      map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)
Tactic:
intro P hP
Proof state after:
case inr
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)
Theorem: Ideal.spanIntNorm_mul
Proof state before:
case inr
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)
Tactic:
by_cases hP0 : P = ⊥
Proof state after:
case pos
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : P = ⊥
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)

case neg
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)
Theorem: Ideal.spanIntNorm_mul
Proof state before:
case neg
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)
Tactic:
let P' := Algebra.algebraMapSubmonoid S P.primeCompl
Proof state after:
case neg
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)
Theorem: Ideal.spanIntNorm_mul
Proof state before:
case neg
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)
Tactic:
let Rₚ := Localization.AtPrime P
Proof state after:
case neg
R : Type u_1
inst✝¹⁵ : CommRing R
S : Type u_2
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
inst✝¹² : IsIntegrallyClosed R
inst✝¹¹ : IsDomain R
inst✝¹⁰ : IsDomain S
inst✝⁹ : NoZeroSMulDivisors R S
hRS : Module.Finite R S
inst✝⁸ : IsIntegrallyClosed S
inst✝⁷ : IsSeparable (FractionRing R) (FractionRing S)
inst✝⁶ : IsDomain R
inst✝⁵ : IsDomain S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDedekindDomain S
inst✝² : Module.Finite R S
inst✝¹ : Module.Free R S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
⊢ map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanIntNorm R I * spanIntNorm R J)