ResidueTorsion.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Torsion in the kernel of a residue map

The geometric-sum argument works for any ring homomorphism from a domain to a field of characteristic p. In a local-ring application the map is the residue homomorphism; the domain itself need not have characteristic p.

theorem OAI.CirculantHadamard.eq_one_of_residue_one_of_not_dvd line 26
Source documentation
A root whose image is one is trivial if one of its torsion exponents is not divisible by the target characteristic.
```
theorem eq_one_of_residue_one_of_not_dvd {p m : ℕ} [CharP K p]
    (f : R →+* K) (z : R) (hmap : f z = 1) (hpow : z ^ m = 1)
    (hm : ¬ p ∣ m) : z = 1 := by
…
```
theorem OAI.CirculantHadamard.eq_one_of_residue_one_of_coprime line 42
Source documentation
Coprime-order torsion in the residue-one subgroup is trivial. The exponent need not be the exact order.
```
theorem eq_one_of_residue_one_of_coprime {p m : ℕ} [CharP K p]
    (f : R →+* K) (z : R) (hp : p.Prime) (hmap : f z = 1)
    (hpow : z ^ m = 1) (hcop : m.Coprime p) : z = 1 := by
…
```
theorem OAI.CirculantHadamard.exists_prime_power_of_residue_one line 48
theorem OAI.CirculantHadamard.orderOf_eq_prime_power_of_residue_one line 62
Source documentation
The exact order is a power of the residue characteristic, including the zeroth power for the identity element.
```
theorem orderOf_eq_prime_power_of_residue_one {p : ℕ} [CharP K p]
    (f : R →+* K) (z : R) (hp : p.Prime) (hmap : f z = 1)
    (hfinite : IsOfFinOrder z) : ∃ a : ℕ, orderOf z = p ^ a := by
…
```
theorem OAI.CirculantHadamard.units_eq_one_of_residue_one_of_odd line 72
Source documentation
The characteristic-two consequence needed for the two alternating products: a unit of odd torsion exponent and residue one equals one.
```
theorem units_eq_one_of_residue_one_of_odd [CharP K 2]
    (f : R →+* K) (u : Rˣ) (hmap : f (u : R) = 1)
    (hfinite : ∃ m : ℕ, 0 < m ∧ Odd m ∧ u ^ m = 1) : u = 1 := by
…
```