mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Int.Range

Goal state before:
pp: m n r : ℤ
⊢ r ∈ m.range n ↔ m ≤ r ∧ r < n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
inst✝¹⁰ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑n
x : CyclotomicField n K
this : NeZero ↑n
y : CyclotomicField n K
hy : y ∈ {b | b ^ n = 1}
⊢ y * (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑(⟨y, ⋯⟩, 1).2 =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) (⟨y, ⋯⟩, 1).1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Range

Goal state before:
pp: P : ℤ → Prop
inst✝ : DecidablePred P
m n : ℤ
⊢ (∀ (r : ℤ), r ∈ m.range n → P r) ↔ ∀ (r : ℤ), m ≤ r → r < n → P r

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Range

Goal state before:
pp: P : ℤ → Prop
inst✝ : DecidablePred P
m n : ℤ
⊢ (∀ (r : ℤ), r ∈ m.range (n + 1) → P r) ↔ ∀ (r : ℤ), m ≤ r → r ≤ n → P r

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: ⊢ ∀ (x y : ZMod 4),
    (match x * y with
      | 0 => 0
      | 2 => 0
      | 1 => 1
      | 3 => -1) =
      (match x with
        | 0 => 0
        | 2 => 0
        | 1 => 1
        | 3 => -1) *
        match y with
        | 0 => 0
        | 2 => 0
        | 1 => 1
        | 3 => -1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: ⊢ ∀ (a : ZMod 4),
    ¬IsUnit a →
      (match a with
        | 0 => 0
        | 2 => 0
        | 1 => 1
        | 3 => -1) =
        0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: ⊢ χ₄.IsQuadratic

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℕ
⊢ χ₄ ↑n = χ₄ ↑(n % 4)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℤ
⊢ χ₄ ↑n = χ₄ ↑(n % 4)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℤ
⊢ ∀ (m : ℤ), 0 ≤ m → m < 4 → χ₄ ↑m = if m % 2 = 0 then 0 else if m = 1 then 1 else -1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 4 → χ₄ ↑m = if m % 2 = 0 then 0 else if m = 1 then 1 else -1
⊢ 2 ∣ 4

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 4 → χ₄ ↑m = if m % 2 = 0 then 0 else if m = 1 then 1 else -1
⊢ 4 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℤ
⊢ χ₄ ↑n = if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℕ
hn : n % 2 = 1
⊢ ∀ m < 4, m % 2 = 1 → (if m = 1 then 1 else -1) = (-1) ^ (m / 2)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℕ
hn : n % 2 = 1
help : ∀ m < 4, m % 2 = 1 → (if m = 1 then 1 else -1) = (-1) ^ (m / 2)
⊢ 0 < 4

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℕ
hn : n % 2 = 1
help : ∀ m < 4, m % 2 = 1 → (if m = 1 then 1 else -1) = (-1) ^ (m / 2)
⊢ 2 ∣ 4

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℕ
hn : n % 2 = 1
⊢ χ₄ ↑n = (-1) ^ (n / 2)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℕ
hn : n % 4 = 1
⊢ χ₄ ↑n = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℕ
hn : n % 4 = 3
⊢ χ₄ ↑n = -1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℤ
hn : n % 4 = 1
⊢ χ₄ ↑n = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℤ
hn : n % 4 = 3
⊢ χ₄ ↑n = -1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: ⊢ ∀ (x y : ZMod 8),
    (match x * y with
      | 0 => 0
      | 2 => 0
      | 4 => 0
      | 6 => 0
      | 1 => 1
      | 7 => 1
      | 3 => -1
      | 5 => -1) =
      (match x with
        | 0 => 0
        | 2 => 0
        | 4 => 0
        | 6 => 0
        | 1 => 1
        | 7 => 1
        | 3 => -1
        | 5 => -1) *
        match y with
        | 0 => 0
        | 2 => 0
        | 4 => 0
        | 6 => 0
        | 1 => 1
        | 7 => 1
        | 3 => -1
        | 5 => -1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: ⊢ ∀ (a : ZMod 8),
    ¬IsUnit a →
      (match a with
        | 0 => 0
        | 2 => 0
        | 4 => 0
        | 6 => 0
        | 1 => 1
        | 7 => 1
        | 3 => -1
        | 5 => -1) =
        0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: ⊢ χ₈.IsQuadratic

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℕ
⊢ χ₈ ↑n = χ₈ ↑(n % 8)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℤ
⊢ χ₈ ↑n = χ₈ ↑(n % 8)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℤ
⊢ ∀ (m : ℤ), 0 ≤ m → m < 8 → χ₈ ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 8 → χ₈ ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1
⊢ 2 ∣ 8

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 8 → χ₈ ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1
⊢ 8 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℤ
⊢ χ₈ ↑n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 7 then 1 else -1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: ⊢ ∀ (x y : ZMod 8),
    (match x * y with
      | 0 => 0
      | 2 => 0
      | 4 => 0
      | 6 => 0
      | 1 => 1
      | 3 => 1
      | 5 => -1
      | 7 => -1) =
      (match x with
        | 0 => 0
        | 2 => 0
        | 4 => 0
        | 6 => 0
        | 1 => 1
        | 3 => 1
        | 5 => -1
        | 7 => -1) *
        match y with
        | 0 => 0
        | 2 => 0
        | 4 => 0
        | 6 => 0
        | 1 => 1
        | 3 => 1
        | 5 => -1
        | 7 => -1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: ⊢ ∀ (a : ZMod 8),
    ¬IsUnit a →
      (match a with
        | 0 => 0
        | 2 => 0
        | 4 => 0
        | 6 => 0
        | 1 => 1
        | 3 => 1
        | 5 => -1
        | 7 => -1) =
        0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: ⊢ χ₈'.IsQuadratic

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℤ
⊢ ∀ (m : ℤ), 0 ≤ m → m < 8 → χ₈' ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 3 then 1 else -1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 8 → χ₈' ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 3 then 1 else -1
⊢ 2 ∣ 8

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 8 → χ₈' ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 3 then 1 else -1
⊢ 8 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℤ
⊢ χ₈' ↑n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 3 then 1 else -1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: ⊢ ∀ (a : ZMod 8), χ₈' a = χ₄ a.cast * χ₈ a

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: a : ℤ
⊢ 4 ∣ 8

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: a : ℤ
⊢ χ₈' ↑a = χ₄ ↑a * χ₈ ↑a

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ₀ χ₁ : MulChar R R'
h : (fun χ ↦ (↑χ.toMonoidHom).toFun) χ₀ = (fun χ ↦ (↑χ.toMonoidHom).toFun) χ₁
⊢ χ₀ = χ₁

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
⊢ R → R'

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
⊢ (if IsUnit 1 then 1 else 0) = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
a : ZMod n
ha : IsUnit a
⊢ χ a = ↑((toUnitHom χ) ha.unit)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ ψ : DirichletCharacter R n
⊢ toUnitHom χ = toUnitHom ψ ↔ χ = ψ

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
x : ZMod n
⊢ χ (↑n - x) = χ (-x)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
inst✝ : Nontrivial R
a : ℤ
⊢ χ ↑a ≠ 0 ↔ IsCoprime a ↑n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
⊢ ∀ (x y : R), (if IsUnit (x * y) then 1 else 0) = (if IsUnit x then 1 else 0) * if IsUnit y then 1 else 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
inst✝ : Nontrivial R
a : ℤ
⊢ χ ↑a = 0 ↔ ¬IsCoprime a ↑n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
⊢ ∀ (a : R), ¬IsUnit a → (if IsUnit a then 1 else 0) = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ : ℕ
χ : DirichletCharacter R n✝
n m : ℕ
hm : n ∣ m
⊢ ofUnitHom ((toUnitHom 1).comp (ZMod.unitsMap hm)) = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n✝ : ℕ
χ : DirichletCharacter R n✝
n m : ℕ
hm : n ∣ m
ψ₁ ψ₂ : DirichletCharacter R n
⊢ ofUnitHom ((toUnitHom (ψ₁ * ψ₂)).comp (ZMod.unitsMap hm)) =
    ofUnitHom ((toUnitHom ψ₁).comp (ZMod.unitsMap hm)) * ofUnitHom ((toUnitHom ψ₂).comp (ZMod.unitsMap hm))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
hm : n ∣ m
⊢ toUnitHom ((changeLevel hm) χ) = (toUnitHom χ).comp (ZMod.unitsMap hm)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ χ' : MulChar R R'
h : ∀ (a : Rˣ), χ ↑a = χ' ↑a
⊢ χ = χ'

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
f : Rˣ →* R'ˣ
⊢ R → R'

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
f : Rˣ →* R'ˣ
⊢ (if hx : IsUnit 1 then ↑(f hx.unit) else 0) = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n m : ℕ
inst✝ : NeZero m
hm : n ∣ m
⊢ Function.Injective ⇑(changeLevel hm)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ (changeLevel ⋯) χ = χ

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ toUnitHom ((changeLevel ⋯) χ) = toUnitHom χ

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m d : ℕ
hm : n ∣ m
hd : m ∣ d
⊢ (changeLevel ⋯) χ = (changeLevel hd) ((changeLevel hm) χ)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
hm : n ∣ m
a : (ZMod m)ˣ
⊢ ((changeLevel hm) χ) ↑a = χ (↑a).cast

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
hm : n ∣ m
a : ℤ
ha : IsCoprime a ↑m
⊢ ((changeLevel hm) χ) ↑a = χ ↑a

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_3
inst✝ : CommMonoidWithZero R'
g : Rˣ
hg : ∀ (x : Rˣ), x ∈ Subgroup.zpowers g
χ₁ χ₂ : MulChar R R'
⊢ χ₁ = χ₂ ↔ χ₁ ↑g = χ₂ ↑g

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst✝ : NeZero n
h : χ.FactorsThrough d
⊢ ∃! χ', χ = (changeLevel ⋯) χ'

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_3
inst✝ : CommMonoidWithZero R'
f : Rˣ →* R'ˣ
S : Submonoid R
⊢ domRestrict S (ofUnitHom f) = ofUnitHom ((f.domRestrict S.units).comp ↑S.unitsEquivUnitsType.symm)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Lemmas

Goal state before:
pp: R : Type u_1
R' : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing R'
inst✝ : StarRing R'
χ : MulChar R R'
⊢ χ.starComp.starComp = χ

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Lemmas

Goal state before:
pp: R : Type u_1
R' : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing R'
inst✝ : StarRing R'
χ χ' : MulChar R R'
⊢ (χ * χ').starComp = χ'.starComp * χ.starComp

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
f : Rˣ →* R'ˣ
⊢ ∀ (x y : R),
    (if hx : IsUnit (x * y) then ↑(f hx.unit) else 0) =
      (if hx : IsUnit x then ↑(f hx.unit) else 0) * if hx : IsUnit y then ↑(f hx.unit) else 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Lemmas

Goal state before:
pp: R : Type u_1
R' : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing R'
inst✝ : Fintype Rˣ
a : Rˣ
χ : MulChar R R'
⊢ (equivToUnitHom χ) a ∈ rootsOfUnity (Fintype.card Rˣ) R'

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
f : Rˣ →* R'ˣ
⊢ ∀ (a : R), ¬IsUnit a → (if hx : IsUnit a then ↑(f hx.unit) else 0) = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
f : Rˣ →* R'ˣ
a : Rˣ
⊢ (ofUnitHom f) ↑a = ↑(f a)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
⊢ Function.LeftInverse ofUnitHom toUnitHom

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
⊢ Function.RightInverse ofUnitHom toUnitHom

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Finite Rˣ
χ : MulChar R ℂ
⊢ star χ = χ⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
inst✝ : Nontrivial R'
χ : MulChar R R'
a : R
⊢ χ a ≠ 0 → IsUnit a

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
inst✝ : Nontrivial R'
χ : MulChar R R'
a : R
⊢ χ a = 0 ↔ ¬IsUnit a

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Finite Rˣ
χ : MulChar R ℂ
a : R
⊢ star (χ a) = χ⁻¹ a

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R' : Type u_2
inst✝² : CommMonoidWithZero R'
R : Type u_3
inst✝¹ : CommMonoidWithZero R
inst✝ : Nontrivial R
χ : MulChar R R'
⊢ χ 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R' : Type u_2
inst✝² : CommMonoidWithZero R'
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
χ : MulChar R R'
⊢ χ ↑(ringChar R) = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
a : Rˣ
⊢ 1 ↑a = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ χ' : MulChar R R'
a : R
ha : ¬IsUnit a
⊢ (⇑χ * ⇑χ') a = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
⊢ 1 * χ = χ

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
⊢ χ * 1 = χ

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
a : R
ha : ¬IsUnit a
⊢ MonoidWithZero.inverse (χ a) = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Lemmas

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
inst✝² : Fintype M
inst✝¹ : DecidableEq M
R : Type u_2
inst✝ : CommMonoidWithZero R
ζ : Rˣ
hζ : ζ ∈ rootsOfUnity (Fintype.card Mˣ) R
g : Mˣ
hg : ∀ (x : Mˣ), x ∈ Subgroup.zpowers g
⊢ MulChar M R

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Lemmas

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
inst✝² : Fintype M
inst✝¹ : DecidableEq M
R : Type u_2
inst✝ : CommMonoidWithZero R
ζ : Rˣ
hζ : ζ ∈ rootsOfUnity (Fintype.card Mˣ) R
g : Mˣ
hg : ∀ (x : Mˣ), x ∈ Subgroup.zpowers g
⊢ (ofRootOfUnity hζ hg) ↑g = ↑ζ

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Lemmas

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
inst✝² : Fintype M
inst✝¹ : DecidableEq M
R : Type u_2
inst✝ : CommMonoidWithZero R
inst_cyc : IsCyclic Mˣ
χ : MulChar M R
⊢ χ.toUnitHom (Classical.choose ⋯) ∈ rootsOfUnity (Fintype.card Mˣ) R

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst✝ : NeZero n
hd : d ∣ n
h : (ZMod.unitsMap hd).ker ≤ (toUnitHom χ).ker
E : (ZMod d)ˣ →* Rˣ := ((ZMod.unitsMap hd).liftOfSurjective ⋯) ⟨toUnitHom χ, h⟩
hE : E.comp (ZMod.unitsMap hd) = toUnitHom χ
⊢ toUnitHom χ = toUnitHom ((changeLevel hd) (ofUnitHom E))

Tactic:
simp_rw [changeLevel_toUnitHom, toUnitHom_eq, ofUnitHom_eq, Equiv.apply_symm_apply, hE,
      toUnitHom_eq]

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Lemmas

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
inst✝² : Fintype M
inst✝¹ : DecidableEq M
R : Type u_2
inst✝ : CommMonoidWithZero R
inst_cyc : IsCyclic Mˣ
χ : MulChar M R
⊢ (fun ζ ↦ ofRootOfUnity ⋯ ⋯) ((fun χ ↦ ⟨χ.toUnitHom (Classical.choose ⋯), ⋯⟩) χ) = χ

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst✝ : NeZero n
hd : d ∣ n
⊢ χ.FactorsThrough d ↔ (ZMod.unitsMap hd).ker ≤ (toUnitHom χ).ker

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Lemmas

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
inst✝² : Fintype M
inst✝¹ : DecidableEq M
R : Type u_2
inst✝ : CommMonoidWithZero R
inst_cyc : IsCyclic Mˣ
ζ : ↥(rootsOfUnity (Fintype.card Mˣ) R)
⊢ (fun χ ↦ ⟨χ.toUnitHom (Classical.choose ⋯), ⋯⟩) ((fun ζ ↦ ofRootOfUnity ⋯ ⋯) ζ) = ζ

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Lemmas

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
inst✝² : Fintype M
inst✝¹ : DecidableEq M
R : Type u_2
inst✝ : CommMonoidWithZero R
inst_cyc : IsCyclic Mˣ
x y : MulChar M R
⊢ ⟨(x * y).toUnitHom (Classical.choose ⋯), ⋯⟩ =
    ⟨x.toUnitHom (Classical.choose ⋯), ⋯⟩ * ⟨y.toUnitHom (Classical.choose ⋯), ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Lemmas

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
R : Type u_2
inst✝ : CommRing R
n : ℕ
h : n ∣ Fintype.card F - 1
ζ : R
hζ : IsPrimitiveRoot ζ n
⊢ 0 < n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R' : Type u_2
inst✝¹ : CommMonoidWithZero R'
R : Type u_3
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
⊢ χ⁻¹ a = χ a⁻¹ʳ

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d m : ℕ
inst✝ : NeZero n
hχ : χ.FactorsThrough d
hd : d ∣ m
hm : m ∣ n
⊢ χ.FactorsThrough m

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
⊢ χ⁻¹ * χ = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
⊢ ∀ (a b c : MulChar R R'), a * b * c = a * (b * c)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
⊢ ∀ (a b : MulChar R R'), a * b = b * a

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
n : ℕ
a : Rˣ
⊢ (χ ^ n) ↑a = χ ↑a ^ n

Tactic:
by

Goal state after: