internlm/Lean-Github huggingface dataset:
Theorem: prod_smul_primesOver
Proof state before:
case pos.a.e_a
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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∈ primesOver S p
this : Fintype ↑(primesOver S p)
⊢ Fintype.card { x // P' = ↑(x • P) } = Fintype.card { x // x • P = P }
Tactic:
obtain ⟨σ, hσ⟩ := MulAction.exists_smul_eq (L ≃ₐ[K] L) P ⟨P', hP'⟩
Proof state after:
case pos.a.e_a.intro
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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∈ primesOver S p
this : Fintype ↑(primesOver S p)
σ : L ≃ₐ[K] L
hσ : σ • P = ⟨P', hP'⟩
⊢ Fintype.card { x // P' = ↑(x • P) } = Fintype.card { x // x • P = P }
Theorem: prod_smul_primesOver
Proof state before:
case pos.a.e_a.intro
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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∈ primesOver S p
this : Fintype ↑(primesOver S p)
σ : L ≃ₐ[K] L
hσ : σ • P = ⟨P', hP'⟩
⊢ Fintype.card { x // P' = ↑(x • P) } = Fintype.card { x // x • P = P }
Tactic:
have : P' = ↑(σ • P) := by rw [hσ]
Proof state after:
case pos.a.e_a.intro
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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝³ : IsDomain S
this✝² : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this✝¹ : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∈ primesOver S p
this✝ : Fintype ↑(primesOver S p)
σ : L ≃ₐ[K] L
hσ : σ • P = ⟨P', hP'⟩
this : P' = ↑(σ • P)
⊢ Fintype.card { x // P' = ↑(x • P) } = Fintype.card { x // x • P = P }
Theorem: prod_smul_primesOver
Proof state before:
case pos.a.e_a.intro
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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝³ : IsDomain S
this✝² : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this✝¹ : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∈ primesOver S p
this✝ : Fintype ↑(primesOver S p)
σ : L ≃ₐ[K] L
hσ : σ • P = ⟨P', hP'⟩
this : P' = ↑(σ • P)
⊢ Fintype.card { x // P' = ↑(x • P) } = Fintype.card { x // x • P = P }
Tactic:
simp_rw [this, ← Subtype.ext_iff, ← eq_inv_smul_iff (a := σ), ← mul_smul, eq_comm (a := P)]
Proof state after:
case pos.a.e_a.intro
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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝³ : IsDomain S
this✝² : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this✝¹ : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∈ primesOver S p
this✝ : Fintype ↑(primesOver S p)
σ : L ≃ₐ[K] L
hσ : σ • P = ⟨P', hP'⟩
this : P' = ↑(σ • P)
⊢ Fintype.card { x // (σ⁻¹ * x) • P = P } = Fintype.card { x // x • P = P }
Theorem: prod_smul_primesOver
Proof state before:
case pos.a.e_a.intro
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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝³ : IsDomain S
this✝² : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this✝¹ : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∈ primesOver S p
this✝ : Fintype ↑(primesOver S p)
σ : L ≃ₐ[K] L
hσ : σ • P = ⟨P', hP'⟩
this : P' = ↑(σ • P)
⊢ Fintype.card { x // (σ⁻¹ * x) • P = P } = Fintype.card { x // x • P = P }
Tactic:
exact Fintype.card_congr
  { toFun := fun x ↦ ⟨σ⁻¹ * x, x.prop⟩,
    invFun := fun x ↦ ⟨σ * x, (inv_mul_cancel_left σ x).symm ▸ x.prop⟩,
    left_inv := fun x ↦ Subtype.ext (mul_inv_cancel_left σ x),
    right_inv := fun x ↦ Subtype.ext (inv_mul_cancel_left σ x) }
Proof state after:
no goals
Theorem: prod_smul_primesOver
Proof 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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this✝ : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∈ primesOver S p
this : Fintype ↑(primesOver S p)
σ : L ≃ₐ[K] L
hσ : σ • P = ⟨P', hP'⟩
⊢ P' = ↑(σ • P)
Tactic:
rw [hσ]
Proof state after:
no goals
Theorem: prod_smul_primesOver
Proof state before:
case neg
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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∉ primesOver S p
⊢ Multiset.count P' (Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val) =
    Ideal.ramificationIdxIn S p * Ideal.inertiaDegIn S p * if P' ∈ primesOver S p then 1 else 0
Tactic:
rw [if_neg hP', mul_zero, Multiset.count_eq_zero]
Proof state after:
case neg
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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∉ primesOver S p
⊢ P' ∉ Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val
Theorem: prod_smul_primesOver
Proof state before:
case neg
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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∉ primesOver S p
⊢ P' ∉ Multiset.map (fun σ => ↑(σ • P)) Finset.univ.val
Tactic:
simp only [Multiset.mem_map, Finset.mem_val, Finset.mem_univ, true_and, not_exists]
Proof state after:
case neg
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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∉ primesOver S p
⊢ ∀ (x : L ≃ₐ[K] L), ¬↑(x • P) = P'
Theorem: prod_smul_primesOver
Proof state before:
case neg
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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
P' : Ideal S
hP' : P' ∉ primesOver S p
⊢ ∀ (x : L ≃ₐ[K] L), ¬↑(x • P) = P'
Tactic:
rintro σ rfl
Proof state after:
case neg
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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
σ : L ≃ₐ[K] L
hP' : ↑(σ • P) ∉ primesOver S p
⊢ False
Theorem: prod_smul_primesOver
Proof state before:
case neg
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✝¹ : IsGalois K L
p : Ideal R
P : ↑(primesOver S p)
inst✝ : p.IsMaximal
this✝¹ : IsDomain S
this✝ : IsDedekindDomain S
hRS : NoZeroSMulDivisors R S
this : IsNoetherian R S
hp : ¬p = ⊥
σ : L ≃ₐ[K] L
hP' : ↑(σ • P) ∉ primesOver S p
⊢ False
Tactic:
exact hP' (σ • P).2
Proof state after:
no goals
Theorem: IsCyclotomicExtension.CyclotomicUnit.associated_one_sub_pow_primitive_root_of_coprime
Proof state before:
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n j k : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
hk : k.Coprime n
hj : j.Coprime n
⊢ Associated (1 - ζ ^ j) (1 - ζ ^ k)
Tactic:
suffices ∀ {j : ℕ}, j.Coprime n → Associated (1 - ζ) (1 - ζ ^ j) by
  exact (this hj).symm.trans (this hk)
Proof state after:
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n j k : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
hk : k.Coprime n
hj : j.Coprime n
⊢ ∀ {j : ℕ}, j.Coprime n → Associated (1 - ζ) (1 - ζ ^ j)
Theorem: IsCyclotomicExtension.CyclotomicUnit.associated_one_sub_pow_primitive_root_of_coprime
Proof state before:
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n j k : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
hk : k.Coprime n
hj : j.Coprime n
⊢ ∀ {j : ℕ}, j.Coprime n → Associated (1 - ζ) (1 - ζ ^ j)
Tactic:
clear k j hk hj
Proof state after:
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
⊢ ∀ {j : ℕ}, j.Coprime n → Associated (1 - ζ) (1 - ζ ^ j)
Theorem: IsCyclotomicExtension.CyclotomicUnit.associated_one_sub_pow_primitive_root_of_coprime
Proof state before:
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
⊢ ∀ {j : ℕ}, j.Coprime n → Associated (1 - ζ) (1 - ζ ^ j)
Tactic:
intro j hj
Proof state after:
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
j : ℕ
hj : j.Coprime n
⊢ Associated (1 - ζ) (1 - ζ ^ j)
Theorem: IsCyclotomicExtension.CyclotomicUnit.associated_one_sub_pow_primitive_root_of_coprime
Proof state before:
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
j : ℕ
hj : j.Coprime n
⊢ Associated (1 - ζ) (1 - ζ ^ j)
Tactic:
refine' associated_of_dvd_dvd ⟨∑ i in range j, ζ ^ i, by rw [← geom_sum_mul_neg, mul_comm]⟩ _
Proof state after:
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
j : ℕ
hj : j.Coprime n
⊢ 1 - ζ ^ j ∣ 1 - ζ
Theorem: IsCyclotomicExtension.CyclotomicUnit.associated_one_sub_pow_primitive_root_of_coprime
Proof state before:
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
j : ℕ
hj : j.Coprime n
⊢ 1 - ζ ^ j ∣ 1 - ζ
Tactic:
rcases eq_or_ne n 0 with (rfl | hn')
Proof state after:
case inl
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
ζ : A
j : ℕ
hζ : IsPrimitiveRoot ζ 0
hj : j.Coprime 0
⊢ 1 - ζ ^ j ∣ 1 - ζ

case inr
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
j : ℕ
hj : j.Coprime n
hn' : n ≠ 0
⊢ 1 - ζ ^ j ∣ 1 - ζ
Theorem: IsCyclotomicExtension.CyclotomicUnit.associated_one_sub_pow_primitive_root_of_coprime
Proof state before:
case inr
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
j : ℕ
hj : j.Coprime n
hn' : n ≠ 0
⊢ 1 - ζ ^ j ∣ 1 - ζ
Tactic:
rcases eq_or_ne n 1 with (rfl | hn)
Proof state after:
case inr.inl
n : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
ζ : A
j : ℕ
hζ : IsPrimitiveRoot ζ 1
hj : j.Coprime 1
hn' : 1 ≠ 0
⊢ 1 - ζ ^ j ∣ 1 - ζ

case inr.inr
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
j : ℕ
hj : j.Coprime n
hn' : n ≠ 0
hn : n ≠ 1
⊢ 1 - ζ ^ j ∣ 1 - ζ
Theorem: IsCyclotomicExtension.CyclotomicUnit.associated_one_sub_pow_primitive_root_of_coprime
Proof state before:
case inr.inr
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
j : ℕ
hj : j.Coprime n
hn' : n ≠ 0
hn : n ≠ 1
⊢ 1 - ζ ^ j ∣ 1 - ζ
Tactic:
replace hn := Nat.one_lt_of_ne n hn' hn
Proof state after:
case inr.inr
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
j : ℕ
hj : j.Coprime n
hn' : n ≠ 0
hn : 1 < n
⊢ 1 - ζ ^ j ∣ 1 - ζ
Theorem: IsCyclotomicExtension.CyclotomicUnit.associated_one_sub_pow_primitive_root_of_coprime
Proof state before:
case inr.inr
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
j : ℕ
hj : j.Coprime n
hn' : n ≠ 0
hn : 1 < n
⊢ 1 - ζ ^ j ∣ 1 - ζ
Tactic:
obtain ⟨m, hm⟩ := Nat.exists_mul_emod_eq_one_of_coprime hj hn
Proof state after:
case inr.inr.intro
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
j : ℕ
hj : j.Coprime n
hn' : n ≠ 0
hn : 1 < n
m : ℕ
hm : j * m % n = 1
⊢ 1 - ζ ^ j ∣ 1 - ζ
Theorem: IsCyclotomicExtension.CyclotomicUnit.associated_one_sub_pow_primitive_root_of_coprime
Proof state before:
case inr.inr.intro
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
j : ℕ
hj : j.Coprime n
hn' : n ≠ 0
hn : 1 < n
m : ℕ
hm : j * m % n = 1
⊢ 1 - ζ ^ j ∣ 1 - ζ
Tactic:
use ∑ i in range m, (ζ ^ j) ^ i
Proof state after:
case h
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
j : ℕ
hj : j.Coprime n
hn' : n ≠ 0
hn : 1 < n
m : ℕ
hm : j * m % n = 1
⊢ 1 - ζ = (1 - ζ ^ j) * ∑ i ∈ range m, (ζ ^ j) ^ i
Theorem: IsCyclotomicExtension.CyclotomicUnit.associated_one_sub_pow_primitive_root_of_coprime
Proof state before:
case h
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
j : ℕ
hj : j.Coprime n
hn' : n ≠ 0
hn : 1 < n
m : ℕ
hm : j * m % n = 1
⊢ 1 - ζ = (1 - ζ ^ j) * ∑ i ∈ range m, (ζ ^ j) ^ i
Tactic:
have : ζ = (ζ ^ j) ^ m := by rw [← pow_mul, ←pow_mod_orderOf, ← hζ.eq_orderOf, hm, pow_one]
Proof state after:
case h
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
j : ℕ
hj : j.Coprime n
hn' : n ≠ 0
hn : 1 < n
m : ℕ
hm : j * m % n = 1
this : ζ = (ζ ^ j) ^ m
⊢ 1 - ζ = (1 - ζ ^ j) * ∑ i ∈ range m, (ζ ^ j) ^ i
Theorem: IsCyclotomicExtension.CyclotomicUnit.associated_one_sub_pow_primitive_root_of_coprime
Proof state before:
case h
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
j : ℕ
hj : j.Coprime n
hn' : n ≠ 0
hn : 1 < n
m : ℕ
hm : j * m % n = 1
this : ζ = (ζ ^ j) ^ m
⊢ 1 - ζ = (1 - ζ ^ j) * ∑ i ∈ range m, (ζ ^ j) ^ i
Tactic:
nth_rw 1 [this]
Proof state after:
case h
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
j : ℕ
hj : j.Coprime n
hn' : n ≠ 0
hn : 1 < n
m : ℕ
hm : j * m % n = 1
this : ζ = (ζ ^ j) ^ m
⊢ 1 - (ζ ^ j) ^ m = (1 - ζ ^ j) * ∑ i ∈ range m, (ζ ^ j) ^ i