internlm/Lean-Github huggingface dataset:
Theorem: rootsOfUnity.integer_power_of_ringEquiv
Proof state before:
L : Type u
inst✝ : Field L
n : ℕ+
g : L ≃+* L
⊢ ∃ m, ∀ (t : { x // x ∈ rootsOfUnity n L }), ↑g ↑↑t = ↑↑(t ^ m)
Tactic:
obtain ⟨m, hm⟩ := MonoidHom.map_cyclic (g.restrictRootsOfUnity n).toMonoidHom
Proof state after:
case intro
L : Type u
inst✝ : Field L
n : ℕ+
g : L ≃+* L
m : ℤ
hm : ∀ (g_1 : { x // x ∈ rootsOfUnity n L }), ↑(MulEquiv.toMonoidHom (RingEquiv.restrictRootsOfUnity g n)) g_1 = g_1 ^ m
⊢ ∃ m, ∀ (t : { x // x ∈ rootsOfUnity n L }), ↑g ↑↑t = ↑↑(t ^ m)
Theorem: rootsOfUnity.integer_power_of_ringEquiv
Proof state before:
case intro
L : Type u
inst✝ : Field L
n : ℕ+
g : L ≃+* L
m : ℤ
hm : ∀ (g_1 : { x // x ∈ rootsOfUnity n L }), ↑(MulEquiv.toMonoidHom (RingEquiv.restrictRootsOfUnity g n)) g_1 = g_1 ^ m
⊢ ∃ m, ∀ (t : { x // x ∈ rootsOfUnity n L }), ↑g ↑↑t = ↑↑(t ^ m)
Tactic:
exact ⟨m, by simp [← hm]⟩
Proof state after:
no goals
Theorem: rootsOfUnity.integer_power_of_ringEquiv
Proof state before:
L : Type u
inst✝ : Field L
n : ℕ+
g : L ≃+* L
m : ℤ
hm : ∀ (g_1 : { x // x ∈ rootsOfUnity n L }), ↑(MulEquiv.toMonoidHom (RingEquiv.restrictRootsOfUnity g n)) g_1 = g_1 ^ m
⊢ ∀ (t : { x // x ∈ rootsOfUnity n L }), ↑g ↑↑t = ↑↑(t ^ m)
Tactic:
simp [← hm]
Proof state after:
no goals
Theorem: Group.pow_eq_zpow_mod
Proof state before:
L : Type u
inst✝¹ : Field L
n✝ : ℕ+
G : Type u_1
inst✝ : Group G
x : G
m : ℤ
n : ℕ
h : x ^ n = 1
⊢ x ^ m = x ^ (m % ↑n)
Tactic:
have h2 : x ^ m = x ^ ((n : ℤ) * (m / (n : ℤ)) + m % (n : ℤ)) :=
  congr_arg (fun a => x ^ a) ((Int.add_comm _ _).trans (Int.emod_add_ediv _ _)).symm
Proof state after:
L : Type u
inst✝¹ : Field L
n✝ : ℕ+
G : Type u_1
inst✝ : Group G
x : G
m : ℤ
n : ℕ
h : x ^ n = 1
h2 : x ^ m = x ^ (↑n * (m / ↑n) + m % ↑n)
⊢ x ^ m = x ^ (m % ↑n)
Theorem: Group.pow_eq_zpow_mod
Proof state before:
L : Type u
inst✝¹ : Field L
n✝ : ℕ+
G : Type u_1
inst✝ : Group G
x : G
m : ℤ
n : ℕ
h : x ^ n = 1
h2 : x ^ m = x ^ (↑n * (m / ↑n) + m % ↑n)
⊢ x ^ m = x ^ (m % ↑n)
Tactic:
simp [h, h2, zpow_add, zpow_mul]
Proof state after:
no goals
Theorem: ModularCyclotomicCharacter.spec
Proof state before:
L : Type u
inst✝ : Field L
n✝ : ℕ+
g : L ≃+* L
n : ℕ+
⊢ ∀ (t : { x // x ∈ rootsOfUnity n L }), ↑g ↑↑t = ↑↑(t ^ ZMod.val (χ n g))
Tactic:
rintro t
Proof state after:
L : Type u
inst✝ : Field L
n✝ : ℕ+
g : L ≃+* L
n : ℕ+
t : { x // x ∈ rootsOfUnity n L }
⊢ ↑g ↑↑t = ↑↑(t ^ ZMod.val (χ n g))
Theorem: ModularCyclotomicCharacter.spec
Proof state before:
L : Type u
inst✝ : Field L
n✝ : ℕ+
g : L ≃+* L
n : ℕ+
t : { x // x ∈ rootsOfUnity n L }
⊢ ↑g ↑↑t = ↑↑(t ^ ZMod.val (χ n g))
Tactic:
rw [ModularCyclotomicCharacter_aux_spec g n t, ← zpow_ofNat, ModularCyclotomicCharacter.toFun,
    ZMod.val_int_cast, ←Group.pow_eq_zpow_mod _ pow_card_eq_one]
Proof state after:
no goals
Theorem: ModularCyclotomicCharacter.ext
Proof state before:
L : Type u
inst✝³ : Field L
n : ℕ+
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : IsCyclic G
d : ℕ
a b : ZMod d
hGcard : Fintype.card G = d
h : ∀ (t : G), t ^ ZMod.val a = t ^ ZMod.val b
⊢ a = b
Tactic:
obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := G)
Proof state after:
case intro
L : Type u
inst✝³ : Field L
n : ℕ+
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : IsCyclic G
d : ℕ
a b : ZMod d
hGcard : Fintype.card G = d
h : ∀ (t : G), t ^ ZMod.val a = t ^ ZMod.val b
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
⊢ a = b
Theorem: ModularCyclotomicCharacter.ext
Proof state before:
case intro
L : Type u
inst✝³ : Field L
n : ℕ+
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : IsCyclic G
d : ℕ
a b : ZMod d
hGcard : Fintype.card G = d
h : ∀ (t : G), t ^ ZMod.val a = t ^ ZMod.val b
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
⊢ a = b
Tactic:
have hgord := orderOf_eq_card_of_forall_mem_zpowers hg
Proof state after:
case intro
L : Type u
inst✝³ : Field L
n : ℕ+
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : IsCyclic G
d : ℕ
a b : ZMod d
hGcard : Fintype.card G = d
h : ∀ (t : G), t ^ ZMod.val a = t ^ ZMod.val b
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
hgord : orderOf g = Fintype.card G
⊢ a = b
Theorem: ModularCyclotomicCharacter.ext
Proof state before:
case intro
L : Type u
inst✝³ : Field L
n : ℕ+
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : IsCyclic G
d : ℕ
a b : ZMod d
hGcard : Fintype.card G = d
h : ∀ (t : G), t ^ ZMod.val a = t ^ ZMod.val b
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
hgord : orderOf g = Fintype.card G
⊢ a = b
Tactic:
specialize h g
Proof state after:
case intro
L : Type u
inst✝³ : Field L
n : ℕ+
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : IsCyclic G
d : ℕ
a b : ZMod d
hGcard : Fintype.card G = d
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
hgord : orderOf g = Fintype.card G
h : g ^ ZMod.val a = g ^ ZMod.val b
⊢ a = b
Theorem: ModularCyclotomicCharacter.ext
Proof state before:
case intro
L : Type u
inst✝³ : Field L
n : ℕ+
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : IsCyclic G
d : ℕ
a b : ZMod d
hGcard : Fintype.card G = d
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
hgord : orderOf g = Fintype.card G
h : g ^ ZMod.val a = g ^ ZMod.val b
⊢ a = b
Tactic:
rw [pow_eq_pow_iff_modEq, hgord, hGcard, ← ZMod.nat_cast_eq_nat_cast_iff] at h
Proof state after:
case intro
L : Type u
inst✝³ : Field L
n : ℕ+
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : IsCyclic G
d : ℕ
a b : ZMod d
hGcard : Fintype.card G = d
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
hgord : orderOf g = Fintype.card G
h : ↑(ZMod.val a) = ↑(ZMod.val b)
⊢ a = b
Theorem: ModularCyclotomicCharacter.ext
Proof state before:
case intro
L : Type u
inst✝³ : Field L
n : ℕ+
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : IsCyclic G
d : ℕ
a b : ZMod d
hGcard : Fintype.card G = d
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
hgord : orderOf g = Fintype.card G
h : ↑(ZMod.val a) = ↑(ZMod.val b)
⊢ a = b
Tactic:
subst hGcard
Proof state after:
case intro
L : Type u
inst✝³ : Field L
n : ℕ+
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : IsCyclic G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
hgord : orderOf g = Fintype.card G
a b : ZMod (Fintype.card G)
h : ↑(ZMod.val a) = ↑(ZMod.val b)
⊢ a = b
Theorem: ModularCyclotomicCharacter.ext
Proof state before:
case intro
L : Type u
inst✝³ : Field L
n : ℕ+
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : IsCyclic G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
hgord : orderOf g = Fintype.card G
a b : ZMod (Fintype.card G)
h : ↑(ZMod.val a) = ↑(ZMod.val b)
⊢ a = b
Tactic:
simpa [ZMod.nat_cast_val, ZMod.cast_id'] using h
Proof state after:
no goals
Theorem: ModularCyclotomicCharacter.id
Proof state before:
L : Type u
inst✝ : Field L
n : ℕ+
⊢ χ n (RingEquiv.refl L) = 1
Tactic:
refine ext (G := rootsOfUnity n L) rfl ?_
Proof state after:
L : Type u
inst✝ : Field L
n : ℕ+
⊢ ∀ (t : { x // x ∈ rootsOfUnity n L }), t ^ ZMod.val (χ n (RingEquiv.refl L)) = t ^ ZMod.val 1
Theorem: ModularCyclotomicCharacter.id
Proof state before:
L : Type u
inst✝ : Field L
n : ℕ+
⊢ ∀ (t : { x // x ∈ rootsOfUnity n L }), t ^ ZMod.val (χ n (RingEquiv.refl L)) = t ^ ZMod.val 1
Tactic:
intro ζ
Proof state after:
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
⊢ ζ ^ ZMod.val (χ n (RingEquiv.refl L)) = ζ ^ ZMod.val 1
Theorem: ModularCyclotomicCharacter.id
Proof state before:
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
⊢ ζ ^ ZMod.val (χ n (RingEquiv.refl L)) = ζ ^ ZMod.val 1
Tactic:
ext
Proof state after:
case a.a
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
⊢ ↑↑(ζ ^ ZMod.val (χ n (RingEquiv.refl L))) = ↑↑(ζ ^ ZMod.val 1)
Theorem: ModularCyclotomicCharacter.id
Proof state before:
case a.a
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
⊢ ↑↑(ζ ^ ZMod.val (χ n (RingEquiv.refl L))) = ↑↑(ζ ^ ZMod.val 1)
Tactic:
rw [← spec]
Proof state after:
case a.a
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
⊢ ↑(RingEquiv.refl L) ↑↑ζ = ↑↑(ζ ^ ZMod.val 1)
Theorem: ModularCyclotomicCharacter.id
Proof state before:
case a.a
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
⊢ ↑(RingEquiv.refl L) ↑↑ζ = ↑↑(ζ ^ ZMod.val 1)
Tactic:
have : 1 ≤ Fintype.card { x // x ∈ rootsOfUnity n L } := Fin.size_positive'
Proof state after:
case a.a
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
this : 1 ≤ Fintype.card { x // x ∈ rootsOfUnity n L }
⊢ ↑(RingEquiv.refl L) ↑↑ζ = ↑↑(ζ ^ ZMod.val 1)
Theorem: ModularCyclotomicCharacter.id
Proof state before:
case a.a
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
this : 1 ≤ Fintype.card { x // x ∈ rootsOfUnity n L }
⊢ ↑(RingEquiv.refl L) ↑↑ζ = ↑↑(ζ ^ ZMod.val 1)
Tactic:
obtain (h | h) := this.lt_or_eq
Proof state after:
case a.a.inl
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
this : 1 ≤ Fintype.card { x // x ∈ rootsOfUnity n L }
h : 1 < Fintype.card { x // x ∈ rootsOfUnity n L }
⊢ ↑(RingEquiv.refl L) ↑↑ζ = ↑↑(ζ ^ ZMod.val 1)

case a.a.inr
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
this : 1 ≤ Fintype.card { x // x ∈ rootsOfUnity n L }
h : 1 = Fintype.card { x // x ∈ rootsOfUnity n L }
⊢ ↑(RingEquiv.refl L) ↑↑ζ = ↑↑(ζ ^ ZMod.val 1)
Theorem: ModularCyclotomicCharacter.id
Proof state before:
case a.a.inl
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
this : 1 ≤ Fintype.card { x // x ∈ rootsOfUnity n L }
h : 1 < Fintype.card { x // x ∈ rootsOfUnity n L }
⊢ ↑(RingEquiv.refl L) ↑↑ζ = ↑↑(ζ ^ ZMod.val 1)
Tactic:
have := Fact.mk h
Proof state after:
case a.a.inl
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
this✝ : 1 ≤ Fintype.card { x // x ∈ rootsOfUnity n L }
h : 1 < Fintype.card { x // x ∈ rootsOfUnity n L }
this : Fact (1 < Fintype.card { x // x ∈ rootsOfUnity n L })
⊢ ↑(RingEquiv.refl L) ↑↑ζ = ↑↑(ζ ^ ZMod.val 1)
Theorem: ModularCyclotomicCharacter.id
Proof state before:
case a.a.inl
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
this✝ : 1 ≤ Fintype.card { x // x ∈ rootsOfUnity n L }
h : 1 < Fintype.card { x // x ∈ rootsOfUnity n L }
this : Fact (1 < Fintype.card { x // x ∈ rootsOfUnity n L })
⊢ ↑(RingEquiv.refl L) ↑↑ζ = ↑↑(ζ ^ ZMod.val 1)
Tactic:
simp [ZMod.val_one]
Proof state after:
no goals
Theorem: ModularCyclotomicCharacter.id
Proof state before:
case a.a.inr
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
this : 1 ≤ Fintype.card { x // x ∈ rootsOfUnity n L }
h : 1 = Fintype.card { x // x ∈ rootsOfUnity n L }
⊢ ↑(RingEquiv.refl L) ↑↑ζ = ↑↑(ζ ^ ZMod.val 1)
Tactic:
have := Fintype.card_le_one_iff_subsingleton.mp h.ge
Proof state after:
case a.a.inr
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
this✝ : 1 ≤ Fintype.card { x // x ∈ rootsOfUnity n L }
h : 1 = Fintype.card { x // x ∈ rootsOfUnity n L }
this : Subsingleton { x // x ∈ rootsOfUnity n L }
⊢ ↑(RingEquiv.refl L) ↑↑ζ = ↑↑(ζ ^ ZMod.val 1)
Theorem: ModularCyclotomicCharacter.id
Proof state before:
case a.a.inr
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
this✝ : 1 ≤ Fintype.card { x // x ∈ rootsOfUnity n L }
h : 1 = Fintype.card { x // x ∈ rootsOfUnity n L }
this : Subsingleton { x // x ∈ rootsOfUnity n L }
⊢ ↑(RingEquiv.refl L) ↑↑ζ = ↑↑(ζ ^ ZMod.val 1)
Tactic:
obtain rfl : ζ = 1 := by apply Subsingleton.elim
Proof state after:
case a.a.inr
L : Type u
inst✝ : Field L
n : ℕ+
this✝ : 1 ≤ Fintype.card { x // x ∈ rootsOfUnity n L }
h : 1 = Fintype.card { x // x ∈ rootsOfUnity n L }
this : Subsingleton { x // x ∈ rootsOfUnity n L }
⊢ ↑(RingEquiv.refl L) ↑↑1 = ↑↑(1 ^ ZMod.val 1)
Theorem: ModularCyclotomicCharacter.id
Proof state before:
case a.a.inr
L : Type u
inst✝ : Field L
n : ℕ+
this✝ : 1 ≤ Fintype.card { x // x ∈ rootsOfUnity n L }
h : 1 = Fintype.card { x // x ∈ rootsOfUnity n L }
this : Subsingleton { x // x ∈ rootsOfUnity n L }
⊢ ↑(RingEquiv.refl L) ↑↑1 = ↑↑(1 ^ ZMod.val 1)
Tactic:
simp
Proof state after:
no goals
Theorem: ModularCyclotomicCharacter.id
Proof state before:
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
this✝ : 1 ≤ Fintype.card { x // x ∈ rootsOfUnity n L }
h : 1 = Fintype.card { x // x ∈ rootsOfUnity n L }
this : Subsingleton { x // x ∈ rootsOfUnity n L }
⊢ ζ = 1
Tactic:
apply Subsingleton.elim
Proof state after:
no goals
Theorem: ModularCyclotomicCharacter.comp
Proof state before:
L : Type u
inst✝ : Field L
n : ℕ+
g h : L ≃+* L
⊢ χ n (g * h) = χ n g * χ n h
Tactic:
refine ext (G := rootsOfUnity n L) rfl ?_
Proof state after:
L : Type u
inst✝ : Field L
n : ℕ+
g h : L ≃+* L
⊢ ∀ (t : { x // x ∈ rootsOfUnity n L }), t ^ ZMod.val (χ n (g * h)) = t ^ ZMod.val (χ n g * χ n h)
Theorem: ModularCyclotomicCharacter.comp
Proof state before:
L : Type u
inst✝ : Field L
n : ℕ+
g h : L ≃+* L
⊢ ∀ (t : { x // x ∈ rootsOfUnity n L }), t ^ ZMod.val (χ n (g * h)) = t ^ ZMod.val (χ n g * χ n h)
Tactic:
intro ζ
Proof state after:
L : Type u
inst✝ : Field L
n : ℕ+
g h : L ≃+* L
ζ : { x // x ∈ rootsOfUnity n L }
⊢ ζ ^ ZMod.val (χ n (g * h)) = ζ ^ ZMod.val (χ n g * χ n h)
Theorem: ModularCyclotomicCharacter.comp
Proof state before:
L : Type u
inst✝ : Field L
n : ℕ+
g h : L ≃+* L
ζ : { x // x ∈ rootsOfUnity n L }
⊢ ζ ^ ZMod.val (χ n (g * h)) = ζ ^ ZMod.val (χ n g * χ n h)
Tactic:
ext
Proof state after:
case a.a
L : Type u
inst✝ : Field L
n : ℕ+
g h : L ≃+* L
ζ : { x // x ∈ rootsOfUnity n L }
⊢ ↑↑(ζ ^ ZMod.val (χ n (g * h))) = ↑↑(ζ ^ ZMod.val (χ n g * χ n h))
Theorem: ModularCyclotomicCharacter.comp
Proof state before:
case a.a
L : Type u
inst✝ : Field L
n : ℕ+
g h : L ≃+* L
ζ : { x // x ∈ rootsOfUnity n L }
⊢ ↑↑(ζ ^ ZMod.val (χ n (g * h))) = ↑↑(ζ ^ ZMod.val (χ n g * χ n h))
Tactic:
rw [← spec]
Proof state after:
case a.a
L : Type u
inst✝ : Field L
n : ℕ+
g h : L ≃+* L
ζ : { x // x ∈ rootsOfUnity n L }
⊢ ↑(g * h) ↑↑ζ = ↑↑(ζ ^ ZMod.val (χ n g * χ n h))
Theorem: ModularCyclotomicCharacter.comp
Proof state before:
case a.a
L : Type u
inst✝ : Field L
n : ℕ+
g h : L ≃+* L
ζ : { x // x ∈ rootsOfUnity n L }
⊢ ↑(g * h) ↑↑ζ = ↑↑(ζ ^ ZMod.val (χ n g * χ n h))
Tactic:
change g (h (ζ : Lˣ)) = _
Proof state after:
case a.a
L : Type u
inst✝ : Field L
n : ℕ+
g h : L ≃+* L
ζ : { x // x ∈ rootsOfUnity n L }
⊢ ↑g (↑h ↑↑ζ) = ↑↑(ζ ^ ZMod.val (χ n g * χ n h))
Theorem: ModularCyclotomicCharacter.comp
Proof state before:
case a.a
L : Type u
inst✝ : Field L
n : ℕ+
g h : L ≃+* L
ζ : { x // x ∈ rootsOfUnity n L }
⊢ ↑g (↑h ↑↑ζ) = ↑↑(ζ ^ ZMod.val (χ n g * χ n h))
Tactic:
rw [spec, spec, mul_comm, ← pow_mul, eq_comm]
Proof state after:
case a.a
L : Type u
inst✝ : Field L
n : ℕ+
g h : L ≃+* L
ζ : { x // x ∈ rootsOfUnity n L }
⊢ ↑↑(ζ ^ ZMod.val (χ n h * χ n g)) = ↑↑(ζ ^ (ZMod.val (χ n h) * ZMod.val (χ n g)))
Theorem: ModularCyclotomicCharacter.comp
Proof state before:
case a.a
L : Type u
inst✝ : Field L
n : ℕ+
g h : L ≃+* L
ζ : { x // x ∈ rootsOfUnity n L }
⊢ ↑↑(ζ ^ ZMod.val (χ n h * χ n g)) = ↑↑(ζ ^ (ZMod.val (χ n h) * ZMod.val (χ n g)))
Tactic:
congr 2
Proof state after:
case a.a.e_self.e_self
L : Type u
inst✝ : Field L
n : ℕ+
g h : L ≃+* L
ζ : { x // x ∈ rootsOfUnity n L }
⊢ ζ ^ ZMod.val (χ n h * χ n g) = ζ ^ (ZMod.val (χ n h) * ZMod.val (χ n g))
Theorem: ModularCyclotomicCharacter.comp
Proof state before:
case a.a.e_self.e_self
L : Type u
inst✝ : Field L
n : ℕ+
g h : L ≃+* L
ζ : { x // x ∈ rootsOfUnity n L }
⊢ ζ ^ ZMod.val (χ n h * χ n g) = ζ ^ (ZMod.val (χ n h) * ZMod.val (χ n g))
Tactic:
simp only [pow_eq_pow_iff_modEq, ← ZMod.nat_cast_eq_nat_cast_iff, SubmonoidClass.coe_pow,
  ZMod.nat_cast_val, Nat.cast_mul, ZMod.cast_mul (m := orderOf ζ) orderOf_dvd_card_univ]
Proof state after:
no goals
Theorem: QuadraticForm.Isotropic_of_zero_quadForm_dim_ge1
Proof state before:
V : Type ?u.12934
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.13476
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module k W
Q : QuadraticForm k W
h₁ : Q = 0
h₂ : Module.rank k W ≠ 0
⊢ Isotropic Q
Tactic:
rw [QuadraticForm.Isotropic, QuadraticForm.Anisotropic]
Proof state after:
V : Type ?u.12934
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.13476
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module k W
Q : QuadraticForm k W
h₁ : Q = 0
h₂ : Module.rank k W ≠ 0
⊢ ¬∀ (x : W), ↑Q x = 0 → x = 0
Theorem: QuadraticForm.Isotropic_of_zero_quadForm_dim_ge1
Proof state before:
V : Type ?u.12934
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.13476
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module k W
Q : QuadraticForm k W
h₁ : Q = 0
h₂ : Module.rank k W ≠ 0
⊢ ¬∀ (x : W), ↑Q x = 0 → x = 0
Tactic:
have h : ∃ (w : W), w ≠ 0 := by
  simpa only [ne_eq, rank_zero_iff_forall_zero, not_forall] using h₂
Proof state after:
V : Type ?u.12934
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.13476
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module k W
Q : QuadraticForm k W
h₁ : Q = 0
h₂ : Module.rank k W ≠ 0
h : ∃ w, w ≠ 0
⊢ ¬∀ (x : W), ↑Q x = 0 → x = 0
Theorem: QuadraticForm.Isotropic_of_zero_quadForm_dim_ge1
Proof state before:
V : Type ?u.12934
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.13476
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module k W
Q : QuadraticForm k W
h₁ : Q = 0
h₂ : Module.rank k W ≠ 0
h : ∃ w, w ≠ 0
⊢ ¬∀ (x : W), ↑Q x = 0 → x = 0
Tactic:
obtain ⟨w, hw⟩ := h
Proof state after:
case intro
V : Type ?u.12934
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.13476
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module k W
Q : QuadraticForm k W
h₁ : Q = 0
h₂ : Module.rank k W ≠ 0
w : W
hw : w ≠ 0
⊢ ¬∀ (x : W), ↑Q x = 0 → x = 0
Theorem: QuadraticForm.Isotropic_of_zero_quadForm_dim_ge1
Proof state before:
case intro
V : Type ?u.12934
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.13476
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module k W
Q : QuadraticForm k W
h₁ : Q = 0
h₂ : Module.rank k W ≠ 0
w : W
hw : w ≠ 0
⊢ ¬∀ (x : W), ↑Q x = 0 → x = 0
Tactic:
have : Q w = 0 := by 
  rw [h₁]
  simp only [zero_apply]
Proof state after:
case intro
V : Type ?u.12934
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.13476
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module k W
Q : QuadraticForm k W
h₁ : Q = 0
h₂ : Module.rank k W ≠ 0
w : W
hw : w ≠ 0
this : ↑Q w = 0
⊢ ¬∀ (x : W), ↑Q x = 0 → x = 0
Theorem: QuadraticForm.Isotropic_of_zero_quadForm_dim_ge1
Proof state before:
case intro
V : Type ?u.12934
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.13476
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module k W
Q : QuadraticForm k W
h₁ : Q = 0
h₂ : Module.rank k W ≠ 0
w : W
hw : w ≠ 0
this : ↑Q w = 0
⊢ ¬∀ (x : W), ↑Q x = 0 → x = 0
Tactic:
tauto
Proof state after:
no goals
Theorem: QuadraticForm.Isotropic_of_zero_quadForm_dim_ge1
Proof state before:
V : Type ?u.12934
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.13476
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module k W
Q : QuadraticForm k W
h₁ : Q = 0
h₂ : Module.rank k W ≠ 0
⊢ ∃ w, w ≠ 0
Tactic:
simpa only [ne_eq, rank_zero_iff_forall_zero, not_forall] using h₂
Proof state after:
no goals
Theorem: QuadraticForm.Isotropic_of_zero_quadForm_dim_ge1
Proof state before:
V : Type ?u.12934
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.13476
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module k W
Q : QuadraticForm k W
h₁ : Q = 0
h₂ : Module.rank k W ≠ 0
w : W
hw : w ≠ 0
⊢ ↑Q w = 0
Tactic:
rw [h₁]
Proof state after:
V : Type ?u.12934
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.13476
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module k W
Q : QuadraticForm k W
h₁ : Q = 0
h₂ : Module.rank k W ≠ 0
w : W
hw : w ≠ 0
⊢ ↑0 w = 0
Theorem: QuadraticForm.Isotropic_of_zero_quadForm_dim_ge1
Proof state before:
V : Type ?u.12934
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module ℚ V
V₂ : Type ?u.13476
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module ℚ V₂
inst✝³ : FiniteDimensional ℚ V
F : QuadraticForm ℚ V
k W : Type
inst✝² : Field k
inst✝¹ : AddCommGroup W
inst✝ : Module k W
Q : QuadraticForm k W
h₁ : Q = 0
h₂ : Module.rank k W ≠ 0
w : W
hw : w ≠ 0
⊢ ↑0 w = 0
Tactic:
simp only [zero_apply]
Proof state after:
no goals
Theorem: QuadraticForm.HasseMinkowski_global_to_local
Proof state before:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.23512
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
h : Isotropic F
⊢ EverywhereLocallyIsotropic F
Tactic:
rw [EverywhereLocallyIsotropic]
Proof state after:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.23512
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
h : Isotropic F
⊢ (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] F)) ∧ Isotropic (baseChange ℝ F)
Theorem: QuadraticForm.HasseMinkowski_global_to_local
Proof state before:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.23512
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
h : Isotropic F
⊢ (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] F)) ∧ Isotropic (baseChange ℝ F)
Tactic:
simp only [Isotropic, Anisotropic, not_forall, exists_prop] at h ⊢
Proof state after:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.23512
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
h : ∃ x, ↑F x = 0 ∧ ¬x = 0
⊢ (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ∃ x, ↑(baseChange ℚ_[p] F) x = 0 ∧ ¬x = 0) ∧
    ∃ x, ↑(baseChange ℝ F) x = 0 ∧ ¬x = 0
Theorem: QuadraticForm.HasseMinkowski_global_to_local
Proof state before:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.23512
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
h : ∃ x, ↑F x = 0 ∧ ¬x = 0
⊢ (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ∃ x, ↑(baseChange ℚ_[p] F) x = 0 ∧ ¬x = 0) ∧
    ∃ x, ↑(baseChange ℝ F) x = 0 ∧ ¬x = 0
Tactic:
push_neg at h
Proof state after:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.23512
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
h : ∃ x, ↑F x = 0 ∧ x ≠ 0
⊢ (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ∃ x, ↑(baseChange ℚ_[p] F) x = 0 ∧ ¬x = 0) ∧
    ∃ x, ↑(baseChange ℝ F) x = 0 ∧ ¬x = 0