[GOAL]
R : Type u
inst✝¹ : AddMonoid R
R' : Type v
inst✝ : CommMonoid R'
ψ : AddChar R R'
⊢ ↑ψ 0 = 1
[PROOFSTEP]
rw [coe_to_fun_apply, ofAdd_zero, map_one]
[GOAL]
R : Type u
inst✝¹ : AddMonoid R
R' : Type v
inst✝ : CommMonoid R'
ψ : AddChar R R'
x y : R
⊢ ↑ψ (x + y) = ↑ψ x * ↑ψ y
[PROOFSTEP]
rw [coe_to_fun_apply, coe_to_fun_apply _ x, coe_to_fun_apply _ y, ofAdd_add, map_mul]
[GOAL]
R : Type u
inst✝¹ : AddMonoid R
R' : Type v
inst✝ : CommMonoid R'
ψ : AddChar R R'
n : ℕ
x : R
⊢ ↑ψ (n • x) = ↑ψ x ^ n
[PROOFSTEP]
rw [coe_to_fun_apply, coe_to_fun_apply _ x, ofAdd_nsmul, map_pow]
[GOAL]
R : Type u
inst✝² : AddCommGroup R
R'✝ : Type v
inst✝¹ : CommMonoid R'✝
R' : Type v
inst✝ : CommGroup R'
ψ : AddChar R R'
n : ℤ
x : R
⊢ ↑ψ (n • x) = ↑ψ x ^ n
[PROOFSTEP]
rw [coe_to_fun_apply, coe_to_fun_apply _ x, ofAdd_zsmul, map_zpow]
[GOAL]
R : Type u
inst✝¹ : AddCommGroup R
R' : Type v
inst✝ : CommMonoid R'
src✝ : CommMonoid (Multiplicative R →* R') := MonoidHom.commMonoid
ψ : AddChar R R'
⊢ ψ⁻¹ * ψ = 1
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
inst✝¹ : AddCommGroup R
R' : Type v
inst✝ : CommMonoid R'
src✝ : CommMonoid (Multiplicative R →* R') := MonoidHom.commMonoid
ψ : AddChar R R'
x : R
⊢ ↑(ψ⁻¹ * ψ) x = ↑1 x
[PROOFSTEP]
rw [AddChar.mul_apply, AddChar.one_apply, inv_apply, ← map_add_mul, add_left_neg, map_zero_one]
[GOAL]
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
⊢ IsNontrivial ψ ↔ ψ ≠ 1
[PROOFSTEP]
refine' not_forall.symm.trans (Iff.not _)
[GOAL]
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
⊢ (∀ (x : R), ↑ψ x = 1) ↔ ψ = 1
[PROOFSTEP]
rw [FunLike.ext_iff]
[GOAL]
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
⊢ (∀ (x : R), ↑ψ x = 1) ↔ ∀ (x : Multiplicative R), ↑ψ x = ↑1 x
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
⊢ ψ⁻¹ = mulShift ψ (-1)
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
x✝ : R
⊢ ↑ψ⁻¹ x✝ = ↑(mulShift ψ (-1)) x✝
[PROOFSTEP]
rw [inv_apply, mulShift_apply, neg_mul, one_mul]
[GOAL]
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
n : ℕ
x : R
⊢ ↑(mulShift ψ ↑n) x = ↑ψ x ^ n
[PROOFSTEP]
rw [mulShift_apply, ← nsmul_eq_mul, map_nsmul_pow]
[GOAL]
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
n : ℕ
⊢ ψ ^ n = mulShift ψ ↑n
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
n : ℕ
x : R
⊢ ↑(ψ ^ n) x = ↑(mulShift ψ ↑n) x
[PROOFSTEP]
rw [show (ψ ^ n) x = ψ x ^ n from rfl, ← mulShift_spec']
[GOAL]
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
a b : R
⊢ mulShift ψ a * mulShift ψ b = mulShift ψ (a + b)
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
a b x✝ : R
⊢ ↑(mulShift ψ a * mulShift ψ b) x✝ = ↑(mulShift ψ (a + b)) x✝
[PROOFSTEP]
rw [mulShift_apply, right_distrib, map_add_mul]
[GOAL]
case h
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
a b x✝ : R
⊢ ↑(mulShift ψ a * mulShift ψ b) x✝ = ↑ψ (a * x✝) * ↑ψ (b * x✝)
[PROOFSTEP]
norm_cast
[GOAL]
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
⊢ mulShift ψ 0 = 1
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
x✝ : R
⊢ ↑(mulShift ψ 0) x✝ = ↑1 x✝
[PROOFSTEP]
rw [mulShift_apply, zero_mul, map_zero_one]
[GOAL]
case h
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
x✝ : R
⊢ 1 = ↑1 x✝
[PROOFSTEP]
norm_cast
[GOAL]
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
hψ : IsPrimitive ψ
⊢ Function.Injective (mulShift ψ)
[PROOFSTEP]
intro a b h
[GOAL]
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
hψ : IsPrimitive ψ
a b : R
h : mulShift ψ a = mulShift ψ b
⊢ a = b
[PROOFSTEP]
apply_fun fun x => x * mulShift ψ (-b) at h 
[GOAL]
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
hψ : IsPrimitive ψ
a b : R
h : mulShift ψ a * mulShift ψ (-b) = mulShift ψ b * mulShift ψ (-b)
⊢ a = b
[PROOFSTEP]
simp only [mulShift_mul, mulShift_zero, add_right_neg] at h 
[GOAL]
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
hψ : IsPrimitive ψ
a b : R
h : mulShift ψ (a + -b) = 1
⊢ a = b
[PROOFSTEP]
have h₂ := hψ (a + -b)
[GOAL]
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
hψ : IsPrimitive ψ
a b : R
h : mulShift ψ (a + -b) = 1
h₂ : a + -b ≠ 0 → IsNontrivial (mulShift ψ (a + -b))
⊢ a = b
[PROOFSTEP]
rw [h, isNontrivial_iff_ne_trivial, ← sub_eq_add_neg, sub_ne_zero] at h₂ 
[GOAL]
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommRing R'
ψ : AddChar R R'
hψ : IsPrimitive ψ
a b : R
h : mulShift ψ (a + -b) = 1
h₂ : a ≠ b → 1 ≠ 1
⊢ a = b
[PROOFSTEP]
exact not_not.mp fun h => h₂ h rfl
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
F : Type u
inst✝ : Field F
ψ : AddChar F R'
hψ : IsNontrivial ψ
⊢ IsPrimitive ψ
[PROOFSTEP]
intro a ha
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
F : Type u
inst✝ : Field F
ψ : AddChar F R'
hψ : IsNontrivial ψ
a : F
ha : a ≠ 0
⊢ IsNontrivial (mulShift ψ a)
[PROOFSTEP]
cases' hψ with x h
[GOAL]
case intro
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
F : Type u
inst✝ : Field F
ψ : AddChar F R'
a : F
ha : a ≠ 0
x : F
h : ↑ψ x ≠ 1
⊢ IsNontrivial (mulShift ψ a)
[PROOFSTEP]
use a⁻¹ * x
[GOAL]
case h
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
F : Type u
inst✝ : Field F
ψ : AddChar F R'
a : F
ha : a ≠ 0
x : F
h : ↑ψ x ≠ 1
⊢ ↑(mulShift ψ a) (a⁻¹ * x) ≠ 1
[PROOFSTEP]
rwa [mulShift_apply, mul_inv_cancel_left₀ ha]
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ+
ζ : C
hζ : ζ ^ ↑n = 1
⊢ (fun a => ζ ^ ZMod.val (↑toAdd a)) 1 = 1
[PROOFSTEP]
simp only [toAdd_one, ZMod.val_zero, pow_zero]
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ+
ζ : C
hζ : ζ ^ ↑n = 1
x y : Multiplicative (ZMod ↑n)
⊢ OneHom.toFun { toFun := fun a => ζ ^ ZMod.val (↑toAdd a), map_one' := (_ : ζ ^ ZMod.val 0 = 1) } (x * y) =
    OneHom.toFun { toFun := fun a => ζ ^ ZMod.val (↑toAdd a), map_one' := (_ : ζ ^ ZMod.val 0 = 1) } x *
      OneHom.toFun { toFun := fun a => ζ ^ ZMod.val (↑toAdd a), map_one' := (_ : ζ ^ ZMod.val 0 = 1) } y
[PROOFSTEP]
dsimp only
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ+
ζ : C
hζ : ζ ^ ↑n = 1
x y : Multiplicative (ZMod ↑n)
⊢ ζ ^ ZMod.val (↑toAdd (x * y)) = ζ ^ ZMod.val (↑toAdd x) * ζ ^ ZMod.val (↑toAdd y)
[PROOFSTEP]
rw [toAdd_mul, ← pow_add, ZMod.val_add (toAdd x) (toAdd y), ← pow_eq_pow_mod _ hζ]
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ+
ζ : C
hζ : ζ ^ ↑n = 1
a : ℕ
⊢ ↑(zmodChar n hζ) ↑a = ζ ^ a
[PROOFSTEP]
rw [pow_eq_pow_mod a hζ, zmodChar_apply, ZMod.val_nat_cast a]
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ+
ψ : AddChar (ZMod ↑n) C
⊢ IsNontrivial ψ ↔ ↑ψ 1 ≠ 1
[PROOFSTEP]
refine' ⟨_, fun h => ⟨1, h⟩⟩
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ+
ψ : AddChar (ZMod ↑n) C
⊢ IsNontrivial ψ → ↑ψ 1 ≠ 1
[PROOFSTEP]
contrapose!
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ+
ψ : AddChar (ZMod ↑n) C
⊢ ↑ψ 1 = 1 → ¬IsNontrivial ψ
[PROOFSTEP]
rintro h₁ ⟨a, ha⟩
[GOAL]
case intro
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ+
ψ : AddChar (ZMod ↑n) C
h₁ : ↑ψ 1 = 1
a : ZMod ↑n
ha : ↑ψ a ≠ 1
⊢ False
[PROOFSTEP]
have ha₁ : a = a.val • (1 : ZMod ↑n) := by rw [nsmul_eq_mul, mul_one]; exact (ZMod.nat_cast_zmod_val a).symm
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ+
ψ : AddChar (ZMod ↑n) C
h₁ : ↑ψ 1 = 1
a : ZMod ↑n
ha : ↑ψ a ≠ 1
⊢ a = ZMod.val a • 1
[PROOFSTEP]
rw [nsmul_eq_mul, mul_one]
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ+
ψ : AddChar (ZMod ↑n) C
h₁ : ↑ψ 1 = 1
a : ZMod ↑n
ha : ↑ψ a ≠ 1
⊢ a = ↑(ZMod.val a)
[PROOFSTEP]
exact (ZMod.nat_cast_zmod_val a).symm
[GOAL]
case intro
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ+
ψ : AddChar (ZMod ↑n) C
h₁ : ↑ψ 1 = 1
a : ZMod ↑n
ha : ↑ψ a ≠ 1
ha₁ : a = ZMod.val a • 1
⊢ False
[PROOFSTEP]
rw [ha₁, map_nsmul_pow, h₁, one_pow] at ha 
[GOAL]
case intro
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ+
ψ : AddChar (ZMod ↑n) C
h₁ : ↑ψ 1 = 1
a : ZMod ↑n
ha : 1 ≠ 1
ha₁ : a = ZMod.val a • 1
⊢ False
[PROOFSTEP]
exact ha rfl
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ+
ψ : AddChar (ZMod ↑n) C
hψ : IsPrimitive ψ
a : ZMod ↑n
⊢ ↑ψ a = 1 ↔ a = 0
[PROOFSTEP]
refine' ⟨fun h => not_imp_comm.mp (hψ a) _, fun ha => by rw [ha, map_zero_one]⟩
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ+
ψ : AddChar (ZMod ↑n) C
hψ : IsPrimitive ψ
a : ZMod ↑n
ha : a = 0
⊢ ↑ψ a = 1
[PROOFSTEP]
rw [ha, map_zero_one]
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ+
ψ : AddChar (ZMod ↑n) C
hψ : IsPrimitive ψ
a : ZMod ↑n
h : ↑ψ a = 1
⊢ ¬IsNontrivial (mulShift ψ a)
[PROOFSTEP]
rw [zmod_char_isNontrivial_iff n (mulShift ψ a), mulShift_apply, mul_one, h, Classical.not_not]
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ
ψ : AddChar (ZMod n) C
hψ : ∀ (a : ZMod n), ↑ψ a = 1 → a = 0
⊢ IsPrimitive ψ
[PROOFSTEP]
refine' fun a ha => (isNontrivial_iff_ne_trivial _).mpr fun hf => _
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ
ψ : AddChar (ZMod n) C
hψ : ∀ (a : ZMod n), ↑ψ a = 1 → a = 0
a : ZMod n
ha : a ≠ 0
hf : mulShift ψ a = 1
⊢ False
[PROOFSTEP]
have h : mulShift ψ a 1 = (1 : AddChar (ZMod n) C) (1 : ZMod n) := congr_fun (congr_arg (↑) hf) 1
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ
ψ : AddChar (ZMod n) C
hψ : ∀ (a : ZMod n), ↑ψ a = 1 → a = 0
a : ZMod n
ha : a ≠ 0
hf : mulShift ψ a = 1
h : ↑(mulShift ψ a) 1 = ↑1 1
⊢ False
[PROOFSTEP]
rw [mulShift_apply, mul_one] at h 
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ
ψ : AddChar (ZMod n) C
hψ : ∀ (a : ZMod n), ↑ψ a = 1 → a = 0
a : ZMod n
ha : a ≠ 0
hf : mulShift ψ a = 1
h : ↑ψ a = ↑1 1
⊢ False
[PROOFSTEP]
norm_cast at h 
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ
ψ : AddChar (ZMod n) C
hψ : ∀ (a : ZMod n), ↑ψ a = 1 → a = 0
a : ZMod n
ha : a ≠ 0
hf : mulShift ψ a = 1
h : ↑ψ a = ↑1 1
⊢ False
[PROOFSTEP]
exact ha (hψ a h)
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ+
ζ : C
h : IsPrimitiveRoot ζ ↑n
⊢ IsPrimitive (zmodChar n (_ : ζ ^ ↑n = 1))
[PROOFSTEP]
apply zmod_char_primitive_of_eq_one_only_at_zero
[GOAL]
case hψ
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ+
ζ : C
h : IsPrimitiveRoot ζ ↑n
⊢ ∀ (a : ZMod ↑n), ↑(zmodChar n (_ : ζ ^ ↑n = 1)) a = 1 → a = 0
[PROOFSTEP]
intro a ha
[GOAL]
case hψ
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ+
ζ : C
h : IsPrimitiveRoot ζ ↑n
a : ZMod ↑n
ha : ↑(zmodChar n (_ : ζ ^ ↑n = 1)) a = 1
⊢ a = 0
[PROOFSTEP]
rw [zmodChar_apply, ← pow_zero ζ] at ha 
[GOAL]
case hψ
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
C : Type v
inst✝ : CommRing C
n : ℕ+
ζ : C
h : IsPrimitiveRoot ζ ↑n
a : ZMod ↑n
ha : ζ ^ ZMod.val a = ζ ^ 0
⊢ a = 0
[PROOFSTEP]
exact (ZMod.val_eq_zero a).mp (IsPrimitiveRoot.pow_inj h (ZMod.val_lt a) n.pos ha)
[GOAL]
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
⊢ PrimitiveAddChar F F'
[PROOFSTEP]
let p := ringChar F
[GOAL]
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
⊢ PrimitiveAddChar F F'
[PROOFSTEP]
haveI hp : Fact p.Prime := ⟨CharP.char_is_prime F _⟩
[GOAL]
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
⊢ PrimitiveAddChar F F'
[PROOFSTEP]
let pp := p.toPNat hp.1.pos
[GOAL]
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := Nat.toPNat p
⊢ PrimitiveAddChar F F'
[PROOFSTEP]
have hp₂ : ¬ringChar F' ∣ p :=
  by
  cases' CharP.char_is_prime_or_zero F' (ringChar F') with hq hq
  · exact mt (Nat.Prime.dvd_iff_eq hp.1 (Nat.Prime.ne_one hq)).mp h.symm
  · rw [hq]
    exact fun hf => Nat.Prime.ne_zero hp.1 (zero_dvd_iff.mp hf)
[GOAL]
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := Nat.toPNat p
⊢ ¬ringChar F' ∣ p
[PROOFSTEP]
cases' CharP.char_is_prime_or_zero F' (ringChar F') with hq hq
[GOAL]
case inl
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := Nat.toPNat p
hq : Nat.Prime (ringChar F')
⊢ ¬ringChar F' ∣ p
[PROOFSTEP]
exact mt (Nat.Prime.dvd_iff_eq hp.1 (Nat.Prime.ne_one hq)).mp h.symm
[GOAL]
case inr
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := Nat.toPNat p
hq : ringChar F' = 0
⊢ ¬ringChar F' ∣ p
[PROOFSTEP]
rw [hq]
[GOAL]
case inr
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := Nat.toPNat p
hq : ringChar F' = 0
⊢ ¬0 ∣ p
[PROOFSTEP]
exact fun hf => Nat.Prime.ne_zero hp.1 (zero_dvd_iff.mp hf)
[GOAL]
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := Nat.toPNat p
hp₂ : ¬ringChar F' ∣ p
⊢ PrimitiveAddChar F F'
[PROOFSTEP]
let ψ := primitiveZModChar pp F' (neZero_iff.mp (NeZero.of_not_dvd F' hp₂))
[GOAL]
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := Nat.toPNat p
hp₂ : ¬ringChar F' ∣ p
ψ : PrimitiveAddChar (ZMod ↑pp) F' := primitiveZModChar pp F' (_ : ↑↑pp ≠ 0)
⊢ PrimitiveAddChar F F'
[PROOFSTEP]
letI : Algebra (ZMod p) F := ZMod.algebra _ _
[GOAL]
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := Nat.toPNat p
hp₂ : ¬ringChar F' ∣ p
ψ : PrimitiveAddChar (ZMod ↑pp) F' := primitiveZModChar pp F' (_ : ↑↑pp ≠ 0)
this : Algebra (ZMod p) F := ZMod.algebra F p
⊢ PrimitiveAddChar F F'
[PROOFSTEP]
let ψ' := ψ.char.comp (AddMonoidHom.toMultiplicative (Algebra.trace (ZMod p) F).toAddMonoidHom)
[GOAL]
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := Nat.toPNat p
hp₂ : ¬ringChar F' ∣ p
ψ : PrimitiveAddChar (ZMod ↑pp) F' := primitiveZModChar pp F' (_ : ↑↑pp ≠ 0)
this : Algebra (ZMod p) F := ZMod.algebra F p
ψ' : Multiplicative F →* CyclotomicField (PrimitiveAddChar.n ψ) F' :=
  MonoidHom.comp (PrimitiveAddChar.char ψ)
    (↑AddMonoidHom.toMultiplicative (LinearMap.toAddMonoidHom (Algebra.trace (ZMod p) F)))
⊢ PrimitiveAddChar F F'
[PROOFSTEP]
have hψ' : IsNontrivial ψ' :=
  by
  obtain ⟨a, ha⟩ := FiniteField.trace_to_zmod_nondegenerate F one_ne_zero
  rw [one_mul] at ha 
  exact ⟨a, fun hf => ha <| (ψ.prim.zmod_char_eq_one_iff pp <| Algebra.trace (ZMod p) F a).mp hf⟩
[GOAL]
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := Nat.toPNat p
hp₂ : ¬ringChar F' ∣ p
ψ : PrimitiveAddChar (ZMod ↑pp) F' := primitiveZModChar pp F' (_ : ↑↑pp ≠ 0)
this : Algebra (ZMod p) F := ZMod.algebra F p
ψ' : Multiplicative F →* CyclotomicField (PrimitiveAddChar.n ψ) F' :=
  MonoidHom.comp (PrimitiveAddChar.char ψ)
    (↑AddMonoidHom.toMultiplicative (LinearMap.toAddMonoidHom (Algebra.trace (ZMod p) F)))
⊢ IsNontrivial ψ'
[PROOFSTEP]
obtain ⟨a, ha⟩ := FiniteField.trace_to_zmod_nondegenerate F one_ne_zero
[GOAL]
case intro
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := Nat.toPNat p
hp₂ : ¬ringChar F' ∣ p
ψ : PrimitiveAddChar (ZMod ↑pp) F' := primitiveZModChar pp F' (_ : ↑↑pp ≠ 0)
this : Algebra (ZMod p) F := ZMod.algebra F p
ψ' : Multiplicative F →* CyclotomicField (PrimitiveAddChar.n ψ) F' :=
  MonoidHom.comp (PrimitiveAddChar.char ψ)
    (↑AddMonoidHom.toMultiplicative (LinearMap.toAddMonoidHom (Algebra.trace (ZMod p) F)))
a : F
ha : ↑(Algebra.trace (ZMod (ringChar F)) F) (1 * a) ≠ 0
⊢ IsNontrivial ψ'
[PROOFSTEP]
rw [one_mul] at ha 
[GOAL]
case intro
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := Nat.toPNat p
hp₂ : ¬ringChar F' ∣ p
ψ : PrimitiveAddChar (ZMod ↑pp) F' := primitiveZModChar pp F' (_ : ↑↑pp ≠ 0)
this : Algebra (ZMod p) F := ZMod.algebra F p
ψ' : Multiplicative F →* CyclotomicField (PrimitiveAddChar.n ψ) F' :=
  MonoidHom.comp (PrimitiveAddChar.char ψ)
    (↑AddMonoidHom.toMultiplicative (LinearMap.toAddMonoidHom (Algebra.trace (ZMod p) F)))
a : F
ha : ↑(Algebra.trace (ZMod (ringChar F)) F) a ≠ 0
⊢ IsNontrivial ψ'
[PROOFSTEP]
exact ⟨a, fun hf => ha <| (ψ.prim.zmod_char_eq_one_iff pp <| Algebra.trace (ZMod p) F a).mp hf⟩
[GOAL]
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := Nat.toPNat p
hp₂ : ¬ringChar F' ∣ p
ψ : PrimitiveAddChar (ZMod ↑pp) F' := primitiveZModChar pp F' (_ : ↑↑pp ≠ 0)
this : Algebra (ZMod p) F := ZMod.algebra F p
ψ' : Multiplicative F →* CyclotomicField (PrimitiveAddChar.n ψ) F' :=
  MonoidHom.comp (PrimitiveAddChar.char ψ)
    (↑AddMonoidHom.toMultiplicative (LinearMap.toAddMonoidHom (Algebra.trace (ZMod p) F)))
hψ' : IsNontrivial ψ'
⊢ PrimitiveAddChar F F'
[PROOFSTEP]
exact ⟨ψ.n, ψ', hψ'.isPrimitive⟩
[GOAL]
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
C : Type v
inst✝² : CommRing C
inst✝¹ : Fintype R
inst✝ : IsDomain R'
ψ : AddChar R R'
hψ : IsNontrivial ψ
⊢ ∑ a : R, ↑ψ a = 0
[PROOFSTEP]
rcases hψ with ⟨b, hb⟩
[GOAL]
case intro
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
C : Type v
inst✝² : CommRing C
inst✝¹ : Fintype R
inst✝ : IsDomain R'
ψ : AddChar R R'
b : R
hb : ↑ψ b ≠ 1
⊢ ∑ a : R, ↑ψ a = 0
[PROOFSTEP]
have h₁ : ∑ a : R, ψ (b + a) = ∑ a : R, ψ a := Fintype.sum_bijective _ (AddGroup.addLeft_bijective b) _ _ fun x => rfl
[GOAL]
case intro
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
C : Type v
inst✝² : CommRing C
inst✝¹ : Fintype R
inst✝ : IsDomain R'
ψ : AddChar R R'
b : R
hb : ↑ψ b ≠ 1
h₁ : ∑ a : R, ↑ψ (b + a) = ∑ a : R, ↑ψ a
⊢ ∑ a : R, ↑ψ a = 0
[PROOFSTEP]
simp_rw [map_add_mul] at h₁ 
[GOAL]
case intro
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
C : Type v
inst✝² : CommRing C
inst✝¹ : Fintype R
inst✝ : IsDomain R'
ψ : AddChar R R'
b : R
hb : ↑ψ b ≠ 1
h₁ : ∑ x : R, ↑ψ b * ↑ψ x = ∑ a : R, ↑ψ a
⊢ ∑ a : R, ↑ψ a = 0
[PROOFSTEP]
have h₂ : ∑ a : R, ψ a = Finset.univ.sum ↑ψ := rfl
[GOAL]
case intro
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
C : Type v
inst✝² : CommRing C
inst✝¹ : Fintype R
inst✝ : IsDomain R'
ψ : AddChar R R'
b : R
hb : ↑ψ b ≠ 1
h₁ : ∑ x : R, ↑ψ b * ↑ψ x = ∑ a : R, ↑ψ a
h₂ : ∑ a : R, ↑ψ a = Finset.sum Finset.univ ↑ψ
⊢ ∑ a : R, ↑ψ a = 0
[PROOFSTEP]
rw [← Finset.mul_sum, h₂] at h₁ 
[GOAL]
case intro
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
C : Type v
inst✝² : CommRing C
inst✝¹ : Fintype R
inst✝ : IsDomain R'
ψ : AddChar R R'
b : R
hb : ↑ψ b ≠ 1
h₁ : ↑ψ b * Finset.sum Finset.univ ↑ψ = Finset.sum Finset.univ ↑ψ
h₂ : ∑ a : R, ↑ψ a = Finset.sum Finset.univ ↑ψ
⊢ ∑ a : R, ↑ψ a = 0
[PROOFSTEP]
exact eq_zero_of_mul_eq_self_left hb h₁
[GOAL]
R : Type u
inst✝³ : CommRing R
R' : Type v
inst✝² : CommRing R'
C : Type v
inst✝¹ : CommRing C
inst✝ : Fintype R
ψ : AddChar R R'
hψ : ¬IsNontrivial ψ
⊢ ∑ a : R, ↑ψ a = ↑(Fintype.card R)
[PROOFSTEP]
simp only [IsNontrivial] at hψ 
[GOAL]
R : Type u
inst✝³ : CommRing R
R' : Type v
inst✝² : CommRing R'
C : Type v
inst✝¹ : CommRing C
inst✝ : Fintype R
ψ : AddChar R R'
hψ : ¬∃ a, ↑ψ a ≠ 1
⊢ ∑ a : R, ↑ψ a = ↑(Fintype.card R)
[PROOFSTEP]
push_neg at hψ 
[GOAL]
R : Type u
inst✝³ : CommRing R
R' : Type v
inst✝² : CommRing R'
C : Type v
inst✝¹ : CommRing C
inst✝ : Fintype R
ψ : AddChar R R'
hψ : ∀ (a : R), ↑ψ a = 1
⊢ ∑ a : R, ↑ψ a = ↑(Fintype.card R)
[PROOFSTEP]
simp only [hψ, Finset.sum_const, Nat.smul_one_eq_coe]
[GOAL]
R : Type u
inst✝³ : CommRing R
R' : Type v
inst✝² : CommRing R'
C : Type v
inst✝¹ : CommRing C
inst✝ : Fintype R
ψ : AddChar R R'
hψ : ∀ (a : R), ↑ψ a = 1
⊢ ↑(Finset.card Finset.univ) = ↑(Fintype.card R)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
inst✝² : Fintype R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R'
ψ : AddChar R R'
b : R
hψ : IsPrimitive ψ
⊢ ∑ x : R, ↑ψ (x * b) = ↑(if b = 0 then Fintype.card R else 0)
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
inst✝² : Fintype R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R'
ψ : AddChar R R'
b : R
hψ : IsPrimitive ψ
h : b = 0
⊢ ∑ x : R, ↑ψ (x * b) = ↑(Fintype.card R)
[PROOFSTEP]
simp only [h, mul_zero, map_zero_one, Finset.sum_const, Nat.smul_one_eq_coe]
[GOAL]
case pos
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
inst✝² : Fintype R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R'
ψ : AddChar R R'
b : R
hψ : IsPrimitive ψ
h : b = 0
⊢ ↑(Finset.card Finset.univ) = ↑(Fintype.card R)
[PROOFSTEP]
rfl
[GOAL]
case neg
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
inst✝² : Fintype R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R'
ψ : AddChar R R'
b : R
hψ : IsPrimitive ψ
h : ¬b = 0
⊢ ∑ x : R, ↑ψ (x * b) = ↑0
[PROOFSTEP]
simp_rw [mul_comm]
[GOAL]
case neg
R : Type u
inst✝⁵ : CommRing R
R' : Type v
inst✝⁴ : CommRing R'
C : Type v
inst✝³ : CommRing C
inst✝² : Fintype R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R'
ψ : AddChar R R'
b : R
hψ : IsPrimitive ψ
h : ¬b = 0
⊢ ∑ x : R, ↑ψ (b * x) = ↑0
[PROOFSTEP]
exact_mod_cast sum_eq_zero_of_isNontrivial (hψ b h)
