Module

PrimeOrderDivisibility.lean

Nyll.ValuedFieldTheory.LocalField.Analytic.PrimeOrderDivisibility

3 declarations indexed from sourceView source ↗

Module documentation

Odd prime order actions trivial modulo the prime

A binomial expansion shows that the augmentation image of such an action on a torsion-free additive group is p-divisible. This does not require finite generation or any topology on the group.

Imports5

Mathlib.Data.Nat.Choose.Sum
Mathlib.Data.Nat.Choose.Dvd
Mathlib.Algebra.Group.Torsion
Mathlib.Algebra.Module.End
Mathlib.Tactic.Abel

Imported by3

theorem

binomial_coefficient_three

L24 ↗

LocalFieldTheory.DiscreteValuationField.binomial_coefficient_three

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory.DiscreteValuationField
open scoped BigOperators

Lean source · statement

theorem binomial_coefficient_three (p : ℕ) (hp : p.Prime) (hp2 : p ≠ 2)
    (j : ℕ) (hj : j < p - 1) :
    p ^ 3 ∣ p.choose (j + 2) * p ^ (j + 2)

theorem

binomial_prime_relation

L36 ↗

LocalFieldTheory.DiscreteValuationField.binomial_prime_relation

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory.DiscreteValuationField
open scoped BigOperators

Lean source · statement

theorem binomial_prime_relation {R : Type*} [Ring R]
    (p : ℕ) (hp : p.Prime) (hp2 : p ≠ 2) (d : R)
    (hpow : (1 + p • d) ^ p = 1) :
    ∃ b : R, p ^ 2 • d = p ^ 3 • (d * b)

theorem

primeOrder_action_sub_divisible

L76 ↗

LocalFieldTheory.DiscreteValuationField.primeOrder_action_sub_divisible

Documentation

An automorphism of odd prime order congruent to the identity modulo that prime has a prime-divisible augmentation image on every torsion-free group.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory.DiscreteValuationField
open scoped BigOperators

Lean source · statement

theorem primeOrder_action_sub_divisible
    {M : Type*} [AddCommGroup M] [IsAddTorsionFree M]
    (T : AddMonoid.End M) (p : ℕ) (hp : p.Prime) (hp2 : p ≠ 2)
    (hT : T ^ p = 1)
    (hdiv : ∀ x : M, ∃ y : M, T x - x = p • y) :
    ∀ x : M, ∃ y : M, T x - x = p • (T y - y)

Module documentation

Odd prime order actions trivial modulo the prime

Declarations

binomial_coefficient_three

binomial_prime_relation

primeOrder_action_sub_divisible