Theorem: KummersLemma.separable_poly (FltRegular/NumberTheory/KummersLemma/Field.lean)

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
⊢ (map (Ideal.Quotient.mk I) (poly hp hζ u hcong)).Separable
Tactic:
let L := K[(p : ℕ)√(u : K)]
State after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
⊢ (map (Ideal.Quotient.mk I) (poly hp hζ u hcong)).Separable

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
⊢ (map (Ideal.Quotient.mk I) (poly hp hζ u hcong)).Separable
Tactic:
letI := Fact.mk (X_pow_sub_C_irreducible_of_prime hpri.out hu)
State after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
⊢ (map (Ideal.Quotient.mk I) (poly hp hζ u hcong)).Separable

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
⊢ (map (Ideal.Quotient.mk I) (poly hp hζ u hcong)).Separable
Tactic:
let J := I.map (algebraMap (𝓞 K) (𝓞 L))
State after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
⊢ (map (Ideal.Quotient.mk I) (poly hp hζ u hcong)).Separable

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
⊢ (map (Ideal.Quotient.mk I) (poly hp hζ u hcong)).Separable
Tactic:
letI : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
State after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this✝ : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
⊢ (map (Ideal.Quotient.mk I) (poly hp hζ u hcong)).Separable

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this✝ : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
⊢ (map (Ideal.Quotient.mk I) (poly hp hζ u hcong)).Separable
Tactic:
letI : Module (𝓞 K) (𝓞 L) := Algebra.toModule
State after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this✝¹ : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this✝ : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
this : Module (𝓞 K) (𝓞 L) := Algebra.toModule
⊢ (map (Ideal.Quotient.mk I) (poly hp hζ u hcong)).Separable

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this✝¹ : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this✝ : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
this : Module (𝓞 K) (𝓞 L) := Algebra.toModule
⊢ (map (Ideal.Quotient.mk I) (poly hp hζ u hcong)).Separable
Tactic:
letI := Ideal.Quotient.commRing J
State after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this✝² : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this✝¹ : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
this✝ : Module (𝓞 K) (𝓞 L) := Algebra.toModule
this : CommRing (𝓞 L ⧸ J) := Ideal.Quotient.commRing J
⊢ (map (Ideal.Quotient.mk I) (poly hp hζ u hcong)).Separable

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this✝² : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this✝¹ : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
this✝ : Module (𝓞 K) (𝓞 L) := Algebra.toModule
this : CommRing (𝓞 L ⧸ J) := Ideal.Quotient.commRing J
⊢ (map (Ideal.Quotient.mk I) (poly hp hζ u hcong)).Separable
Tactic:
let i : 𝓞 K ⧸ I →+* 𝓞 L ⧸ J := Ideal.quotientMap _
  (algebraMap (𝓞 K) (𝓞 L)) Ideal.le_comap_map
State after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this✝² : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this✝¹ : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
this✝ : Module (𝓞 K) (𝓞 L) := Algebra.toModule
this : CommRing (𝓞 L ⧸ J) := Ideal.Quotient.commRing J
i : 𝓞 K ⧸ I →+* 𝓞 L ⧸ J := Ideal.quotientMap J (algebraMap (𝓞 K) (𝓞 L)) ⋯
⊢ (map (Ideal.Quotient.mk I) (poly hp hζ u hcong)).Separable

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this✝³ : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this✝² : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
this✝¹ : Module (𝓞 K) (𝓞 L) := Algebra.toModule
this✝ : CommRing (𝓞 L ⧸ J) := Ideal.Quotient.commRing J
i : 𝓞 K ⧸ I →+* 𝓞 L ⧸ J := Ideal.quotientMap J (algebraMap (𝓞 K) (𝓞 L)) ⋯
this : Nontrivial (𝓞 L ⧸ J)
⊢ (map (Ideal.Quotient.mk I) (poly hp hζ u hcong)).Separable
Tactic:
rw [← Polynomial.separable_map' i, map_map, Ideal.quotientMap_comp_mk, ← map_map]
State after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this✝³ : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this✝² : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
this✝¹ : Module (𝓞 K) (𝓞 L) := Algebra.toModule
this✝ : CommRing (𝓞 L ⧸ J) := Ideal.Quotient.commRing J
i : 𝓞 K ⧸ I →+* 𝓞 L ⧸ J := Ideal.quotientMap J (algebraMap (𝓞 K) (𝓞 L)) ⋯
this : Nontrivial (𝓞 L ⧸ J)
⊢ (map (Ideal.Quotient.mk J) (map (algebraMap (𝓞 K) (𝓞 L)) (poly hp hζ u hcong))).Separable

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this✝³ : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this✝² : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
this✝¹ : Module (𝓞 K) (𝓞 L) := Algebra.toModule
this✝ : CommRing (𝓞 L ⧸ J) := Ideal.Quotient.commRing J
i : 𝓞 K ⧸ I →+* 𝓞 L ⧸ J := Ideal.quotientMap J (algebraMap (𝓞 K) (𝓞 L)) ⋯
this : Nontrivial (𝓞 L ⧸ J)
⊢ (map (Ideal.Quotient.mk J) (map (algebraMap (𝓞 K) (𝓞 L)) (poly hp hζ u hcong))).Separable
Tactic:
apply Separable.map
State after:
case h
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this✝³ : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this✝² : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
this✝¹ : Module (𝓞 K) (𝓞 L) := Algebra.toModule
this✝ : CommRing (𝓞 L ⧸ J) := Ideal.Quotient.commRing J
i : 𝓞 K ⧸ I →+* 𝓞 L ⧸ J := Ideal.quotientMap J (algebraMap (𝓞 K) (𝓞 L)) ⋯
this : Nontrivial (𝓞 L ⧸ J)
⊢ (map (algebraMap (𝓞 K) (𝓞 L)) (poly hp hζ u hcong)).Separable

State before:
case h
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this✝³ : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this✝² : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
this✝¹ : Module (𝓞 K) (𝓞 L) := Algebra.toModule
this✝ : CommRing (𝓞 L ⧸ J) := Ideal.Quotient.commRing J
i : 𝓞 K ⧸ I →+* 𝓞 L ⧸ J := Ideal.quotientMap J (algebraMap (𝓞 K) (𝓞 L)) ⋯
this : Nontrivial (𝓞 L ⧸ J)
⊢ (map (algebraMap (𝓞 K) (𝓞 L)) (poly hp hζ u hcong)).Separable
Tactic:
apply separable_poly_aux hp hζ u hcong
State after:
case h.e
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this✝³ : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this✝² : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
this✝¹ : Module (𝓞 K) (𝓞 L) := Algebra.toModule
this✝ : CommRing (𝓞 L ⧸ J) := Ideal.Quotient.commRing J
i : 𝓞 K ⧸ I →+* 𝓞 L ⧸ J := Ideal.quotientMap J (algebraMap (𝓞 K) (𝓞 L)) ⋯
this : Nontrivial (𝓞 L ⧸ J)
⊢ ?h.α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)

case h.α
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this✝³ : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this✝² : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
this✝¹ : Module (𝓞 K) (𝓞 L) := Algebra.toModule
this✝ : CommRing (𝓞 L ⧸ J) := Ideal.Quotient.commRing J
i : 𝓞 K ⧸ I →+* 𝓞 L ⧸ J := Ideal.quotientMap J (algebraMap (𝓞 K) (𝓞 L)) ⋯
this : Nontrivial (𝓞 L ⧸ J)
⊢ L

State before:
case h.e
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this✝³ : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this✝² : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
this✝¹ : Module (𝓞 K) (𝓞 L) := Algebra.toModule
this✝ : CommRing (𝓞 L ⧸ J) := Ideal.Quotient.commRing J
i : 𝓞 K ⧸ I →+* 𝓞 L ⧸ J := Ideal.quotientMap J (algebraMap (𝓞 K) (𝓞 L)) ⋯
this : Nontrivial (𝓞 L ⧸ J)
⊢ ?h.α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)

case h.α
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this✝³ : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this✝² : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
this✝¹ : Module (𝓞 K) (𝓞 L) := Algebra.toModule
this✝ : CommRing (𝓞 L ⧸ J) := Ideal.Quotient.commRing J
i : 𝓞 K ⧸ I →+* 𝓞 L ⧸ J := Ideal.quotientMap J (algebraMap (𝓞 K) (𝓞 L)) ⋯
this : Nontrivial (𝓞 L ⧸ J)
⊢ L
Tactic:
exact root_X_pow_sub_C_pow _ _
State after:
no goals

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this✝² : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this✝¹ : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
this✝ : Module (𝓞 K) (𝓞 L) := Algebra.toModule
this : CommRing (𝓞 L ⧸ J) := Ideal.Quotient.commRing J
i : 𝓞 K ⧸ I →+* 𝓞 L ⧸ J := Ideal.quotientMap J (algebraMap (𝓞 K) (𝓞 L)) ⋯
⊢ Nontrivial (𝓞 L ⧸ J)
Tactic:
apply Ideal.Quotient.nontrivial
State after:
case hI
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this✝² : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this✝¹ : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
this✝ : Module (𝓞 K) (𝓞 L) := Algebra.toModule
this : CommRing (𝓞 L ⧸ J) := Ideal.Quotient.commRing J
i : 𝓞 K ⧸ I →+* 𝓞 L ⧸ J := Ideal.quotientMap J (algebraMap (𝓞 K) (𝓞 L)) ⋯
⊢ J ≠ ⊤

State before:
case hI
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this✝² : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this✝¹ : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
this✝ : Module (𝓞 K) (𝓞 L) := Algebra.toModule
this : CommRing (𝓞 L ⧸ J) := Ideal.Quotient.commRing J
i : 𝓞 K ⧸ I →+* 𝓞 L ⧸ J := Ideal.quotientMap J (algebraMap (𝓞 K) (𝓞 L)) ⋯
⊢ J ≠ ⊤
Tactic:
rw [ne_eq, Ideal.map_eq_top_iff]
State after:
case hI
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this✝² : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this✝¹ : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
this✝ : Module (𝓞 K) (𝓞 L) := Algebra.toModule
this : CommRing (𝓞 L ⧸ J) := Ideal.Quotient.commRing J
i : 𝓞 K ⧸ I →+* 𝓞 L ⧸ J := Ideal.quotientMap J (algebraMap (𝓞 K) (𝓞 L)) ⋯
⊢ ¬I = ⊤

case hI.hf₁
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this✝² : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this✝¹ : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
this✝ : Module (𝓞 K) (𝓞 L) := Algebra.toModule
this : CommRing (𝓞 L ⧸ J) := Ideal.Quotient.commRing J
i : 𝓞 K ⧸ I →+* 𝓞 L ⧸ J := Ideal.quotientMap J (algebraMap (𝓞 K) (𝓞 L)) ⋯
⊢ Function.Injective ⇑(algebraMap (𝓞 K) (𝓞 L))

case hI.hf₂
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this✝² : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this✝¹ : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
this✝ : Module (𝓞 K) (𝓞 L) := Algebra.toModule
this : CommRing (𝓞 L ⧸ J) := Ideal.Quotient.commRing J
i : 𝓞 K ⧸ I →+* 𝓞 L ⧸ J := Ideal.quotientMap J (algebraMap (𝓞 K) (𝓞 L)) ⋯
⊢ (algebraMap (𝓞 K) (𝓞 L)).IsIntegral

State before:
case hI
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this✝² : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this✝¹ : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
this✝ : Module (𝓞 K) (𝓞 L) := Algebra.toModule
this : CommRing (𝓞 L ⧸ J) := Ideal.Quotient.commRing J
i : 𝓞 K ⧸ I →+* 𝓞 L ⧸ J := Ideal.quotientMap J (algebraMap (𝓞 K) (𝓞 L)) ⋯
⊢ ¬I = ⊤

case hI.hf₁
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this✝² : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this✝¹ : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
this✝ : Module (𝓞 K) (𝓞 L) := Algebra.toModule
this : CommRing (𝓞 L ⧸ J) := Ideal.Quotient.commRing J
i : 𝓞 K ⧸ I →+* 𝓞 L ⧸ J := Ideal.quotientMap J (algebraMap (𝓞 K) (𝓞 L)) ⋯
⊢ Function.Injective ⇑(algebraMap (𝓞 K) (𝓞 L))

case hI.hf₂
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this✝² : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this✝¹ : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
this✝ : Module (𝓞 K) (𝓞 L) := Algebra.toModule
this : CommRing (𝓞 L ⧸ J) := Ideal.Quotient.commRing J
i : 𝓞 K ⧸ I →+* 𝓞 L ⧸ J := Ideal.quotientMap J (algebraMap (𝓞 K) (𝓞 L)) ⋯
⊢ (algebraMap (𝓞 K) (𝓞 L)).IsIntegral
Tactic:
exact Ideal.IsMaximal.ne_top ‹_›
State after:
case hI.hf₁
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this✝² : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this✝¹ : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
this✝ : Module (𝓞 K) (𝓞 L) := Algebra.toModule
this : CommRing (𝓞 L ⧸ J) := Ideal.Quotient.commRing J
i : 𝓞 K ⧸ I →+* 𝓞 L ⧸ J := Ideal.quotientMap J (algebraMap (𝓞 K) (𝓞 L)) ⋯
⊢ Function.Injective ⇑(algebraMap (𝓞 K) (𝓞 L))

case hI.hf₂
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this✝² : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this✝¹ : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
this✝ : Module (𝓞 K) (𝓞 L) := Algebra.toModule
this : CommRing (𝓞 L ⧸ J) := Ideal.Quotient.commRing J
i : 𝓞 K ⧸ I →+* 𝓞 L ⧸ J := Ideal.quotientMap J (algebraMap (𝓞 K) (𝓞 L)) ⋯
⊢ (algebraMap (𝓞 K) (𝓞 L)).IsIntegral

State before:
case hI.hf₁
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this✝² : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this✝¹ : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
this✝ : Module (𝓞 K) (𝓞 L) := Algebra.toModule
this : CommRing (𝓞 L ⧸ J) := Ideal.Quotient.commRing J
i : 𝓞 K ⧸ I →+* 𝓞 L ⧸ J := Ideal.quotientMap J (algebraMap (𝓞 K) (𝓞 L)) ⋯
⊢ Function.Injective ⇑(algebraMap (𝓞 K) (𝓞 L))
Tactic:
intros x y e
State after:
case hI.hf₁
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this✝² : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this✝¹ : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
this✝ : Module (𝓞 K) (𝓞 L) := Algebra.toModule
this : CommRing (𝓞 L ⧸ J) := Ideal.Quotient.commRing J
i : 𝓞 K ⧸ I →+* 𝓞 L ⧸ J := Ideal.quotientMap J (algebraMap (𝓞 K) (𝓞 L)) ⋯
x y : 𝓞 K
e : (algebraMap (𝓞 K) (𝓞 L)) x = (algebraMap (𝓞 K) (𝓞 L)) y
⊢ x = y

State before:
case hI.hf₁
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this✝² : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this✝¹ : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
this✝ : Module (𝓞 K) (𝓞 L) := Algebra.toModule
this : CommRing (𝓞 L ⧸ J) := Ideal.Quotient.commRing J
i : 𝓞 K ⧸ I →+* 𝓞 L ⧸ J := Ideal.quotientMap J (algebraMap (𝓞 K) (𝓞 L)) ⋯
x y : 𝓞 K
e : (algebraMap (𝓞 K) (𝓞 L)) x = (algebraMap (𝓞 K) (𝓞 L)) y
⊢ x = y
Tactic:
ext
State after:
case hI.hf₁.h
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this✝² : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this✝¹ : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
this✝ : Module (𝓞 K) (𝓞 L) := Algebra.toModule
this : CommRing (𝓞 L ⧸ J) := Ideal.Quotient.commRing J
i : 𝓞 K ⧸ I →+* 𝓞 L ⧸ J := Ideal.quotientMap J (algebraMap (𝓞 K) (𝓞 L)) ⋯
x y : 𝓞 K
e : (algebraMap (𝓞 K) (𝓞 L)) x = (algebraMap (𝓞 K) (𝓞 L)) y
⊢ ↑x = ↑y

State before:
case hI.hf₁.h
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this✝² : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this✝¹ : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
this✝ : Module (𝓞 K) (𝓞 L) := Algebra.toModule
this : CommRing (𝓞 L ⧸ J) := Ideal.Quotient.commRing J
i : 𝓞 K ⧸ I →+* 𝓞 L ⧸ J := Ideal.quotientMap J (algebraMap (𝓞 K) (𝓞 L)) ⋯
x y : 𝓞 K
e : (algebraMap (𝓞 K) (𝓞 L)) x = (algebraMap (𝓞 K) (𝓞 L)) y
⊢ ↑x = ↑y
Tactic:
exact (algebraMap K L).injective (congr_arg Subtype.val e)
State after:
no goals

State before:
case hI.hf₂
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this✝² : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this✝¹ : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
this✝ : Module (𝓞 K) (𝓞 L) := Algebra.toModule
this : CommRing (𝓞 L ⧸ J) := Ideal.Quotient.commRing J
i : 𝓞 K ⧸ I →+* 𝓞 L ⧸ J := Ideal.quotientMap J (algebraMap (𝓞 K) (𝓞 L)) ⋯
⊢ (algebraMap (𝓞 K) (𝓞 L)).IsIntegral
Tactic:
intros x
State after:
case hI.hf₂
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this✝² : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this✝¹ : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
this✝ : Module (𝓞 K) (𝓞 L) := Algebra.toModule
this : CommRing (𝓞 L ⧸ J) := Ideal.Quotient.commRing J
i : 𝓞 K ⧸ I →+* 𝓞 L ⧸ J := Ideal.quotientMap J (algebraMap (𝓞 K) (𝓞 L)) ⋯
x : 𝓞 L
⊢ (algebraMap (𝓞 K) (𝓞 L)).IsIntegralElem x

State before:
case hI.hf₂
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
I : Ideal (𝓞 K)
inst✝ : I.IsMaximal
L : Type u_1 := K[↑p√(algebraMap (𝓞 K) K) ↑u]
this✝² : Fact (Irreducible (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))) :=
  { out := X_pow_sub_C_irreducible_of_prime Fact.out hu }
J : Ideal (𝓞 L) := Ideal.map (algebraMap (𝓞 K) (𝓞 L)) I
this✝¹ : AddCommGroup (𝓞 L) := AddCommGroupWithOne.toAddCommGroup
this✝ : Module (𝓞 K) (𝓞 L) := Algebra.toModule
this : CommRing (𝓞 L ⧸ J) := Ideal.Quotient.commRing J
i : 𝓞 K ⧸ I →+* 𝓞 L ⧸ J := Ideal.quotientMap J (algebraMap (𝓞 K) (𝓞 L)) ⋯
x : 𝓞 L
⊢ (algebraMap (𝓞 K) (𝓞 L)).IsIntegralElem x
Tactic:
exact IsIntegral.tower_top (IsIntegralClosure.isIntegral ℤ L x)
State after:
no goals