mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝² : Field K
θ✝ : 𝓞 K
inst✝¹ : NumberField K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
h₀ : Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ) ≠ 0
⊢ span {Polynomial.map (Int.castRingHom (ZMod p)) Q} =
    span {Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)} ⊔ span {Polynomial.map (Int.castRingHom (ZMod p)) Q}

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_2
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : Algebra.IsIntegral ℚ K
inst✝¹ : IsTotallyComplex K
inst✝ : IsGalois ℚ K
σ : Gal(K/ℚ)
hσ : ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ
φ : K →+* ℂ := Classical.choice ⋯
⊢ Nat.card ↥(Subgroup.zpowers σ) = 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_2
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : Algebra.IsIntegral ℚ K
inst✝¹ : IsTotallyComplex K
inst✝ : IsGalois ℚ K
σ : Gal(K/ℚ)
hσ : ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ
φ : K →+* ℂ := Classical.choice ⋯
hσ' : Nat.card ↥(Subgroup.zpowers σ) = 2
⊢ Nat.card ↥(Subgroup.zpowers σ) ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_2
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : Algebra.IsIntegral ℚ K
inst✝¹ : IsTotallyComplex K
inst✝ : IsGalois ℚ K
σ : Gal(K/ℚ)
hσ : ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ
φ : K →+* ℂ := Classical.choice ⋯
hσ' : Nat.card ↥(Subgroup.zpowers σ) = 2
this : Finite ↥(Subgroup.zpowers σ)
L : IntermediateField ℚ K := FixedPoints.intermediateField ↥(Subgroup.zpowers σ)
w : InfinitePlace ↥L
⊢ w.IsReal

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_2
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : Algebra.IsIntegral ℚ K
inst✝¹ : IsTotallyComplex K
inst✝ : IsGalois ℚ K
σ : Gal(K/ℚ)
hσ : ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ
φ : K →+* ℂ := Classical.choice ⋯
hσ' : Nat.card ↥(Subgroup.zpowers σ) = 2
this✝ : Finite ↥(Subgroup.zpowers σ)
L : IntermediateField ℚ K := FixedPoints.intermediateField ↥(Subgroup.zpowers σ)
this : IsTotallyReal ↥L
⊢ Module.finrank (↥L) K = 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_2
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : Algebra.IsIntegral ℚ K
inst✝¹ : IsTotallyComplex K
inst✝ : IsGalois ℚ K
σ : Gal(K/ℚ)
hσ : ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ
⊢ IsCMField K

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁸ : Field F
inst✝⁷ : IsTotallyReal F
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : Algebra.IsIntegral ℚ K
inst✝³ : IsTotallyComplex K
inst✝² : Algebra F K
inst✝¹ : IsQuadraticExtension F K
inst✝ : IsAbelianGalois ℚ K
φ : K →+* ℂ := Classical.choice ⋯
σ : Gal(K/ℚ)
hσ₁ : ComplexEmbedding.IsConj φ σ
ψ : K →+* ℂ
⊢ φ.comp (algebraMap ℚ K) = ψ.comp (algebraMap ℚ K)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ |(↑(completeBasis K).equivFunL.symm).det| = ↑(finrank ℚ K) * regulator K

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ expMapBasis.source = Set.univ

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁸ : Field F
inst✝⁷ : IsTotallyReal F
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : Algebra.IsIntegral ℚ K
inst✝³ : IsTotallyComplex K
inst✝² : Algebra F K
inst✝¹ : IsQuadraticExtension F K
inst✝ : IsAbelianGalois ℚ K
φ : K →+* ℂ := Classical.choice ⋯
σ : Gal(K/ℚ)
hσ₁ : ComplexEmbedding.IsConj φ σ
⊢ ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁸ : Field F
inst✝⁷ : IsTotallyReal F
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : Algebra.IsIntegral ℚ K
inst✝³ : IsTotallyComplex K
inst✝² : Algebra F K
inst✝¹ : IsQuadraticExtension F K
inst✝ : IsAbelianGalois ℚ K
⊢ IsCMField K

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
S : Set ℕ
inst✝ : IsCyclotomicExtension S ℚ K
this : Algebra.IsIntegral ℚ K
n : ℕ
hn₁ : n ∈ S
hn₂ : 2 < n
⊢ n ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
S : Set ℕ
inst✝ : IsCyclotomicExtension S ℚ K
this✝ : Algebra.IsIntegral ℚ K
n : ℕ
hn₁ : n ∈ S
hn₂ : 2 < n
this : NeZero n
⊢ n ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝² : Field K
θ✝ : 𝓞 K
inst✝¹ : NumberField K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
h₀ : Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ) ≠ 0
h_eq₁ :
  span {Polynomial.map (Int.castRingHom (ZMod p)) Q} =
    span {Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)} ⊔ span {Polynomial.map (Int.castRingHom (ZMod p)) Q}
⊢ span {↑p} ⊔ span {(aeval θ) Q} = span {↑p, (aeval θ) Q}

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
S : Set ℕ
inst✝ : IsCyclotomicExtension S ℚ K
this✝ : Algebra.IsIntegral ℚ K
n : ℕ
hn₁ : n ∈ S
hn₂ : 2 < n
this : NeZero n
ζ : K
hζ : IsPrimitiveRoot ζ n
⊢ IsTotallyComplex K

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
⊢ ↑(finrank ℚ K) * regOfFamily u =
    |∑ j,
          (reindex f.symm f.symm)
            (of fun i w ↦ if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(u (e ⟨i, h⟩)))))
            (f.symm w') j| *
      |(((reindex f.symm f.symm)
                (of fun i w ↦
                  if h : i = w' then ↑w.mult
                  else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(u (e ⟨i, h⟩)))))).submatrix
            (f.symm w').succAbove (f.symm w').succAbove).det|

pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
⊢ ∀ (i : Fin (rank K + 1)),
    i ≠ f.symm w' →
      ∑ j,
          (reindex f.symm f.symm)
            (of fun i w ↦ if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(u (e ⟨i, h⟩)))))
            i j =
        0

Tactic:
· simp_rw [reindex_apply, submatrix_submatrix, ← f.symm.sum_comp, f.symm_symm, submatrix_apply,
      Function.comp_def, Equiv.apply_symm_apply, of_apply, dif_pos, ← Nat.cast_sum, sum_mult_eq,
      Nat.abs_cast]
    rw [regOfFamily_eq_det u w' e, ← Matrix.det_reindex_self g]
    congr with i j
    rw [reindex_apply, submatrix_apply, submatrix_apply, of_apply, of_apply, dif_neg]
    rfl

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
⊢ ∀ (i : Fin (rank K + 1)),
    i ≠ f.symm w' →
      ∑ j,
          (reindex f.symm f.symm)
            (of fun i w ↦ if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(u (e ⟨i, h⟩)))))
            i j =
        0
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
S : Set ℕ
hS : ∃ n ∈ S, 2 < n
inst✝ : IsCyclotomicExtension S ℚ K
⊢ IsCMField K

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ ↑expMapBasis x = Real.exp (x w₀) • fun w ↦ ∏ i, w ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ x ↑i

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝² : Field K
θ✝ : 𝓞 K
inst✝¹ : NumberField K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
h₀ : Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ) ≠ 0
h_eq₁ :
  span {Polynomial.map (Int.castRingHom (ZMod p)) Q} =
    span {Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)} ⊔ span {Polynomial.map (Int.castRingHom (ZMod p)) Q}
h_eq₂ : span {↑p} ⊔ span {(aeval θ) Q} = span {↑p, (aeval θ) Q}
⊢ Ideal.map (Ideal.Quotient.mk (span {↑p})) (span {(aeval θ) Q}) =
    Ideal.map (↑(ZModXQuotSpanEquivQuotSpan hp))
      (Ideal.map (Ideal.Quotient.mk (span {Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)}))
        (span {Polynomial.map (Int.castRingHom (ZMod p)) Q}))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
A : ℤ[X]
⊢ ∀ (x : (ℤ ⧸ span {↑p})[X]),
    normalize ((mapEquiv (Int.quotientSpanNatEquivZMod p)).toMulEquiv x) =
      (mapEquiv (Int.quotientSpanNatEquivZMod p)).toMulEquiv (normalize x)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
A : ℤ[X]
x✝ : (ZMod p)[X]
⊢ x✝ ∈
      normalizedFactors
        ((mapEquiv (Int.quotientSpanNatEquivZMod p)).toMulEquiv (Polynomial.map (Ideal.Quotient.mk (span {↑p})) A)) ↔
    x✝ ∈ (normalizedFactors (Polynomial.map (Int.castRingHom (ZMod p)) A)).toFinset

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
⊢ span {↑p} ≠ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
h : span {↑p} ≠ ⊥
⊢ (span {↑p}).primesOver (𝓞 K) = {J | J ∈ normalizedFactors (Ideal.map (algebraMap ℤ (𝓞 K)) (span {↑p}))}

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
⊢ ↑(finrank ℚ K) * regOfFamily u =
    |(of fun i w ↦ if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(u (e ⟨i, h⟩))))).det|

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
Q : (ZMod p)[X]
hQ : Q ∈ monicFactorsMod θ p
⊢ span {↑p} ≠ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ IsMaxRank (fundSystem K)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ basisOfIsMaxRank ⋯ = Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p f : ℕ
hK : Fintype.card K = p ^ f
h0 : f = 0
⊢ Fintype.card K ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
Q : (ZMod p)[X]
hQ : Q ∈ monicFactorsMod θ p
⊢ Polynomial.map (↑(Int.quotientSpanNatEquivZMod p).symm) Q ∈
    {d | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk (span {↑p})) (minpoly ℤ θ))}

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ regulator K = regOfFamily (fundSystem K)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ ↑expMapBasis x = Real.exp (x w₀) • ↑expMapBasis fun i ↦ if i = w₀ then 0 else x i

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ regulator K = |(Matrix.of fun i ↦ (logEmbedding K) (Additive.ofMul (fundSystem K ((equivFinRank K).symm i)))).det|

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this✝² : Fact (Irreducible P)
this✝¹ : Module.Finite K (AdjoinRoot P)
this✝ : Finite (AdjoinRoot P)
this : NeZero ↑n
⊢ NeZero ↑n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
⊢ regulator K = |(Matrix.of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(fundSystem K (e i))))).det|

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
⊢ ↑(finrank ℚ K) * regulator K =
    |(Matrix.of fun i w ↦
          if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(fundSystem K (e ⟨i, h⟩))))).det|

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this✝¹ : Fact (Irreducible P)
this✝ : Module.Finite K (AdjoinRoot P)
this : Finite (AdjoinRoot P)
⊢ NeZero ↑n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this✝² : Fact (Irreducible P)
this✝¹ : Module.Finite K (AdjoinRoot P)
this✝ : Finite (AdjoinRoot P)
this : NeZero ↑n
⊢ map (of P) P ∣ cyclotomic n (AdjoinRoot P)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this✝¹ : Fact (Irreducible P)
this✝ : Module.Finite K (AdjoinRoot P)
this : Finite (AdjoinRoot P)
⊢ IsPrimitiveRoot (root P) n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this✝¹ : Fact (Irreducible P)
this✝ : Module.Finite K (AdjoinRoot P)
this : Finite (AdjoinRoot P)
hζ : IsPrimitiveRoot (root P) n
pB : PowerBasis K (AdjoinRoot P) := powerBasis ⋯
h0 : n = 0
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
⊢ ↑((primesOverSpanEquivMonicFactorsMod hp).symm ⟨Polynomial.map (Int.castRingHom (ZMod p)) Q, hQ⟩) =
    span {↑p, (aeval θ) Q}

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ ∏ w, ↑expMapBasis x w ^ w.mult = Real.exp (x w₀) ^ finrank ℚ K

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ mixedEmbedding.norm (mixedSpaceOfRealSpace (↑expMapBasis x)) = Real.exp (x w₀) ^ finrank ℚ K

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
⊢ (span {↑p, (aeval θ) Q}).LiesOver (span {↑p})

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
⊢ (span {↑p, (aeval θ) Q}).IsMaximal

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u v : Fin (rank K) → (𝓞 K)ˣ
hv : IsMaxRank v
h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K
hu : IsMaxRank u
⊢ span ℤ (Set.range ⇑(basisOfIsMaxRank hu)) ≤ span ℤ (Set.range ⇑(basisOfIsMaxRank hv))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : InfinitePlace K
hw : w ≠ w₀
⊢ mixedEmbedding.norm
      (mixedSpaceOfRealSpace (↑expMap ((completeBasis K).equivFun.symm fun i ↦ if i = w₀ then 0 else x i))) =
    1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this✝¹ : Fact (Irreducible P)
this✝ : Module.Finite K (AdjoinRoot P)
this : Finite (AdjoinRoot P)
hζ : IsPrimitiveRoot (root P) n
pB : PowerBasis K (AdjoinRoot P) := powerBasis ⋯
hζ' : IsOfFinOrder (root P)
φ : Gal(AdjoinRoot P/K) := frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P)
⊢ (φ ^ orderOf φ) (root P) = root P

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
this✝ : (span {↑p, (aeval θ) Q}).IsMaximal
this : (span {↑p, (aeval θ) Q}).LiesOver (span {↑p})
⊢ (algebraMap (ZMod p) ((ZMod p)[X] ⧸ span {Polynomial.map (Int.castRingHom (ZMod p)) Q})).comp
      (Int.quotientSpanNatEquivZMod p).toRingHom =
    (RingEquiv.toRingHom ?m.136).comp (algebraMap (ℤ ⧸ span {↑p}) (𝓞 K ⧸ span {↑p, (aeval θ) Q}))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
⊢ (↑((primesOverSpanEquivMonicFactorsMod hp).symm ⟨Polynomial.map (Int.castRingHom (ZMod p)) Q, hQ⟩)).inertiaDeg ℤ =
    (Polynomial.map (Int.castRingHom (ZMod p)) Q).natDegree

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
Q : (ZMod p)[X]
hQ : Q ∈ monicFactorsMod θ p
⊢ (↑((primesOverSpanEquivMonicFactorsMod hp).symm ⟨Q, hQ⟩)).inertiaDeg ℤ = Q.natDegree

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
⊢ span {↑p} ≠ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
⊢ P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ logMap (mixedSpaceOfRealSpace (↑expMapBasis x)) ∈
      ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) ↔
    ∀ (w : InfinitePlace K), w ≠ w₀ → x w ∈ Set.Ico 0 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hPirr : Irreducible P
A : K[X]
hA : cyclotomic n K = P * A
⊢ P * A = P * (C P.leadingCoeff⁻¹ * C P.leadingCoeff) * A

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hPirr : Irreducible P
A : K[X]
hA : cyclotomic n K = P * A
⊢ P * (C P.leadingCoeff⁻¹ * C P.leadingCoeff) * A = P * C P.leadingCoeff⁻¹ * (A * C P.leadingCoeff)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
s : Set (realSpace K)
⊢ normAtAllPlaces '' normAtAllPlaces ⁻¹' ↑expMapBasis '' s = ↑expMapBasis '' s

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hPirr : Irreducible P
A : K[X]
hA : cyclotomic n K = P * A
⊢ P * C P.leadingCoeff⁻¹ ∣ cyclotomic n K

Tactic:
by

Goal state after: