Theorem: isUnramifiedAt_iff_SquareFree_minpoly_powerBasis (FltRegular/NumberTheory/Unramified.lean)

State before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : NoZeroSMulDivisors R S
inst✝² : IsDedekindDomain S
inst✝¹ : Algebra.IsIntegral R S
pb : PowerBasis R S
p : Ideal R
inst✝ : p.IsPrime
hpbot : p ≠ ⊥
⊢ IsUnramifiedAt S p ↔ Squarefree (Polynomial.map (Ideal.Quotient.mk p) (minpoly R pb.gen))
Tactic:
rw [isUnramifiedAt_iff_SquareFree_minpoly p hpbot pb.gen _ _]
State after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : NoZeroSMulDivisors R S
inst✝² : IsDedekindDomain S
inst✝¹ : Algebra.IsIntegral R S
pb : PowerBasis R S
p : Ideal R
inst✝ : p.IsPrime
hpbot : p ≠ ⊥
⊢ Ideal.comap (algebraMap R S) (conductor R pb.gen) ⊔ p = ⊤

R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : NoZeroSMulDivisors R S
inst✝² : IsDedekindDomain S
inst✝¹ : Algebra.IsIntegral R S
pb : PowerBasis R S
p : Ideal R
inst✝ : p.IsPrime
hpbot : p ≠ ⊥
⊢ IsIntegral R pb.gen

State before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : NoZeroSMulDivisors R S
inst✝² : IsDedekindDomain S
inst✝¹ : Algebra.IsIntegral R S
pb : PowerBasis R S
p : Ideal R
inst✝ : p.IsPrime
hpbot : p ≠ ⊥
⊢ Ideal.comap (algebraMap R S) (conductor R pb.gen) ⊔ p = ⊤

R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : NoZeroSMulDivisors R S
inst✝² : IsDedekindDomain S
inst✝¹ : Algebra.IsIntegral R S
pb : PowerBasis R S
p : Ideal R
inst✝ : p.IsPrime
hpbot : p ≠ ⊥
⊢ IsIntegral R pb.gen
Tactic:
rw [conductor_eq_top_of_powerBasis, Ideal.comap_top, top_sup_eq]
State after:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : NoZeroSMulDivisors R S
inst✝² : IsDedekindDomain S
inst✝¹ : Algebra.IsIntegral R S
pb : PowerBasis R S
p : Ideal R
inst✝ : p.IsPrime
hpbot : p ≠ ⊥
⊢ IsIntegral R pb.gen

State before:
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : IsDedekindDomain R
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra S L
inst✝⁹ : Algebra K L
inst✝⁸ : Algebra R L
inst✝⁷ : IsScalarTower R S L
inst✝⁶ : IsScalarTower R K L
inst✝⁵ : IsIntegralClosure S R L
inst✝⁴ : FiniteDimensional K L
inst✝³ : NoZeroSMulDivisors R S
inst✝² : IsDedekindDomain S
inst✝¹ : Algebra.IsIntegral R S
pb : PowerBasis R S
p : Ideal R
inst✝ : p.IsPrime
hpbot : p ≠ ⊥
⊢ IsIntegral R pb.gen
Tactic:
exact PowerBasis.isIntegral_gen pb
State after:
no goals