Module

AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.lean

Nyll.AlgebraicCurves.Foundations.Algebra.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent

51 declarations indexed from sourceView source ↗

Module documentation

Add Comm Group nat Card torsion By pow eq pow of nat Card fixed primary Component

Imports5

Mathlib.Algebra.Module.Torsion.Basic
Mathlib.Algebra.Ring.GeomSum
Mathlib.Tactic.Ext
Mathlib.Tactic.Positivity
Mathlib.Tactic.Ring.RingNF

Imported by1

Nyll.AlgebraicCurves.Foundations.Algebra.All

abbrev

tor

L37 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.tor

Documentation

The subgroup of elements annihilated by multiplication by m.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section General
variable {A : Type*} [AddCommGroup A]

Lean source · statement

abbrev tor (A : Type*) [AddCommGroup A] (m : ℕ) : AddSubgroup A

theorem

mem_tor

L40 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.mem_tor

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section General
variable {A : Type*} [AddCommGroup A]

Lean source · statement

theorem mem_tor {m : ℕ} {x : A} : x ∈ tor A m ↔ m • x = 0

theorem

tor_le_tor_mul

L43 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.tor_le_tor_mul

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section General
variable {A : Type*} [AddCommGroup A]

Lean source · statement

theorem tor_le_tor_mul (m m' : ℕ) : tor A m ≤ tor A (m' * m)

theorem

card_eq_card_range_mul_card_ker

L48 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.card_eq_card_range_mul_card_ker

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section General
variable {A : Type*} [AddCommGroup A]

Lean source · statement

theorem card_eq_card_range_mul_card_ker {B C : Type*} [AddCommGroup B] [AddCommGroup C]
    (f : B →+ C) : Nat.card B = Nat.card f.range * Nat.card f.ker

theorem

finite_of_finite_range_ker

L53 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.finite_of_finite_range_ker

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section General
variable {A : Type*} [AddCommGroup A]

Lean source · statement

theorem finite_of_finite_range_ker {B C : Type*} [AddCommGroup B] [AddCommGroup C]
    (f : B →+ C) [Finite f.range] [Finite f.ker] : Finite B

theorem

finite_of_le

L59 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.finite_of_le

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section General
variable {A : Type*} [AddCommGroup A]

Lean source · statement

theorem finite_of_le {H K : AddSubgroup A} (h : H ≤ K) [Finite K] : Finite H

theorem

card_ker_mul_le

L62 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.card_ker_mul_le

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section General
variable {A : Type*} [AddCommGroup A]

Lean source · statement

theorem card_ker_mul_le {B : Type*} [AddCommGroup B] (f g : AddMonoid.End B)
    [Finite (f : B →+ B).ker] [Finite (g : B →+ B).ker] :
    Finite ((f * g : AddMonoid.End B) : B →+ B).ker ∧
      Nat.card ((f * g : AddMonoid.End B) : B →+ B).ker ≤
        Nat.card (f : B →+ B).ker * Nat.card (g : B →+ B).ker

abbrev

T

L99 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.T

Documentation

The subgroup of elements annihilated by ℓ ^ n.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Layers
variable {A : Type*} [AddCommGroup A] (ℓ : ℕ)

Lean source · statement

abbrev T (n : ℕ) : AddSubgroup A

theorem

T_le_succ

L101 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.T_le_succ

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Layers
variable {A : Type*} [AddCommGroup A] (ℓ : ℕ)

Lean source · statement

theorem T_le_succ (n : ℕ) : T (A := A) ℓ n ≤ T ℓ (n + 1)

theorem

T_mono

L105 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.T_mono

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Layers
variable {A : Type*} [AddCommGroup A] (ℓ : ℕ)

Lean source · statement

theorem T_mono {n m : ℕ} (h : n ≤ m) : T (A := A) ℓ n ≤ T ℓ m

theorem

T_zero

L110 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.T_zero

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Layers
variable {A : Type*} [AddCommGroup A] (ℓ : ℕ)

Lean source · statement

theorem T_zero : T (A := A) ℓ 0 = ⊥

def

layMap

L115 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.layMap

Documentation

Multiply the (n + 1)st torsion layer by ℓ ^ n and include its image in A.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Layers
variable {A : Type*} [AddCommGroup A] (ℓ : ℕ)

Lean source · statement

def layMap (n : ℕ) : T (A := A) ℓ (n + 1) →+ A

theorem

layMap_apply

L118 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.layMap_apply

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Layers
variable {A : Type*} [AddCommGroup A] (ℓ : ℕ)

Lean source · statement

theorem layMap_apply (n : ℕ) (x : T (A := A) ℓ (n + 1)) :
    layMap ℓ n x = ℓ ^ n • (x : A)

def

I

L122 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.I

Documentation

The image in A of the (n + 1)st torsion layer under multiplication by ℓ ^ n.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Layers
variable {A : Type*} [AddCommGroup A] (ℓ : ℕ)

Lean source · statement

def I (n : ℕ) : AddSubgroup A

theorem

mem_I

L124 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.mem_I

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Layers
variable {A : Type*} [AddCommGroup A] (ℓ : ℕ)

Lean source · statement

theorem mem_I {n : ℕ} {x : A} :
    x ∈ I ℓ n ↔ ∃ y : A, ℓ ^ (n + 1) • y = 0 ∧ ℓ ^ n • y = x

theorem

I_le_T_one

L132 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.I_le_T_one

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Layers
variable {A : Type*} [AddCommGroup A] (ℓ : ℕ)

Lean source · statement

theorem I_le_T_one (n : ℕ) : I (A := A) ℓ n ≤ T ℓ 1

theorem

I_succ_le

L137 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.I_succ_le

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Layers
variable {A : Type*} [AddCommGroup A] (ℓ : ℕ)

Lean source · statement

theorem I_succ_le (n : ℕ) : I (A := A) ℓ (n + 1) ≤ I ℓ n

theorem

I_antitone

L144 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.I_antitone

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Layers
variable {A : Type*} [AddCommGroup A] (ℓ : ℕ)

Lean source · statement

theorem I_antitone : Antitone (I (A := A) ℓ)

theorem

ker_layMap

L146 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.ker_layMap

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Layers
variable {A : Type*} [AddCommGroup A] (ℓ : ℕ)

Lean source · statement

theorem ker_layMap (n : ℕ) :
    (layMap (A := A) ℓ n).ker = (T ℓ n).addSubgroupOf (T ℓ (n + 1))

theorem

card_T_succ

L151 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.card_T_succ

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Layers
variable {A : Type*} [AddCommGroup A] (ℓ : ℕ)

Lean source · statement

theorem card_T_succ (n : ℕ) :
    Nat.card (T (A := A) ℓ (n + 1)) = Nat.card (I (A := A) ℓ n) * Nat.card (T (A := A) ℓ n)

theorem

finite_T

L160 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.finite_T

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Layers
variable {A : Type*} [AddCommGroup A] (ℓ : ℕ)
variable [hℓ : Fact ℓ.Prime]
omit hℓ in

Lean source · statement

theorem finite_T [Finite (tor A ℓ)] (n : ℕ) : Finite (T (A := A) ℓ n)

theorem

finite_I

L175 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.finite_I

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Layers
variable {A : Type*} [AddCommGroup A] (ℓ : ℕ)
variable [hℓ : Fact ℓ.Prime]
omit hℓ in

Lean source · statement

theorem finite_I [Finite (tor A ℓ)] (n : ℕ) : Finite (I (A := A) ℓ n)

theorem

card_I_le

L179 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.card_I_le

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Layers
variable {A : Type*} [AddCommGroup A] (ℓ : ℕ)
variable [hℓ : Fact ℓ.Prime]
omit hℓ in

Lean source · statement

theorem card_I_le [Finite (tor A ℓ)] (n : ℕ) : Nat.card (I (A := A) ℓ n) ≤ Nat.card (tor A ℓ)

theorem

exists_stable

L184 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.exists_stable

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Layers
variable {A : Type*} [AddCommGroup A] (ℓ : ℕ)
variable [hℓ : Fact ℓ.Prime]
omit hℓ in

Lean source · statement

theorem exists_stable [Finite (tor A ℓ)] :
    ∃ n₀ : ℕ, ∀ n, n₀ ≤ n → I (A := A) ℓ n = I ℓ n₀

abbrev

eker

L207 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.eker

Documentation

The kernel of an additive endomorphism of H.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Divisible
variable {H : Type*} [AddCommGroup H] (ℓ : ℕ) [hℓ : Fact ℓ.Prime]

Lean source · statement

abbrev eker (f : AddMonoid.End H) : AddSubgroup H

theorem

mem_eker

L209 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.mem_eker

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Divisible
variable {H : Type*} [AddCommGroup H] (ℓ : ℕ) [hℓ : Fact ℓ.Prime]

Lean source · statement

theorem mem_eker {f : AddMonoid.End H} {x : H} : x ∈ eker f ↔ f x = 0

theorem

natCast_apply

L211 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.natCast_apply

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Divisible
variable {H : Type*} [AddCommGroup H] (ℓ : ℕ) [hℓ : Fact ℓ.Prime]

Lean source · statement

theorem natCast_apply (n : ℕ) (x : H) : (n : AddMonoid.End H) x = n • x

theorem

bijective_one_add

L214 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.bijective_one_add

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Divisible
variable {H : Type*} [AddCommGroup H] (ℓ : ℕ) [hℓ : Fact ℓ.Prime]
omit hℓ in

Lean source · statement

theorem bijective_one_add (hprim : ∀ x : H, ∃ m : ℕ, ℓ ^ m • x = 0) (N : AddMonoid.End H) :
    Function.Bijective (1 + (ℓ : AddMonoid.End H) * N : AddMonoid.End H)

theorem

surjective_nsmul_sq

L260 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.surjective_nsmul_sq

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Divisible
variable {H : Type*} [AddCommGroup H] (ℓ : ℕ) [hℓ : Fact ℓ.Prime]
omit hℓ in

Lean source · statement

theorem surjective_nsmul_sq (hdiv : ∀ x : H, ∃ y : H, ℓ • y = x) :
    Function.Surjective (nsmulAddMonoidHom (ℓ ^ 2) : H →+ H)

theorem

exists_sub_one_eq

L267 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.exists_sub_one_eq

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Divisible
variable {H : Type*} [AddCommGroup H] (ℓ : ℕ) [hℓ : Fact ℓ.Prime]
omit hℓ in

Lean source · statement

theorem exists_sub_one_eq (hdiv : ∀ x : H, ∃ y : H, ℓ • y = x)
    (θ : AddMonoid.End H) (hθ : ∀ x : H, ℓ ^ 2 • x = 0 → θ x = x) :
    ∃ M : AddMonoid.End H, θ - 1 = ((ℓ ^ 2 : ℕ) : AddMonoid.End H) * M

theorem

geom_sum_one_add

L293 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.geom_sum_one_add

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Divisible
variable {H : Type*} [AddCommGroup H] (ℓ : ℕ) [hℓ : Fact ℓ.Prime]

Lean source · statement

theorem geom_sum_one_add {R : Type*} [Ring R] (a : R) (n : ℕ) :
    ∃ G : R, ∑ i ∈ Finset.range n, (1 + a) ^ i = n + G * a

theorem

card_ker_geom_sum

L305 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.card_ker_geom_sum

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Divisible
variable {H : Type*} [AddCommGroup H] (ℓ : ℕ) [hℓ : Fact ℓ.Prime]
omit hℓ in

Lean source · statement

theorem card_ker_geom_sum (hprim : ∀ x : H, ∃ m : ℕ, ℓ ^ m • x = 0)
    (hdiv : ∀ x : H, ∃ y : H, ℓ • y = x) [Finite (tor H ℓ)] (θ : AddMonoid.End H)
    (hθ : ∀ x : H, ℓ ^ 2 • x = 0 → θ x = x) :
    Finite (eker (∑ i ∈ Finset.range ℓ, θ ^ i)) ∧
      Nat.card (eker (∑ i ∈ Finset.range ℓ, θ ^ i)) = Nat.card (tor H ℓ)

theorem

card_fix_pow_le

L328 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.card_fix_pow_le

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Divisible
variable {H : Type*} [AddCommGroup H] (ℓ : ℕ) [hℓ : Fact ℓ.Prime]
omit hℓ in

Lean source · statement

theorem card_fix_pow_le (hprim : ∀ x : H, ∃ m : ℕ, ℓ ^ m • x = 0)
    (hdiv : ∀ x : H, ∃ y : H, ℓ • y = x) [Finite (tor H ℓ)] (θ : AddMonoid.End H)
    (hθ : ∀ x : H, ℓ ^ 2 • x = 0 → θ x = x) [Finite (eker (θ - 1))] (k : ℕ) :
    Finite (eker (θ ^ ℓ ^ k - 1)) ∧
      Nat.card (eker (θ ^ ℓ ^ k - 1)) ≤ Nat.card (eker (θ - 1)) * Nat.card (tor H ℓ) ^ k

theorem

le_of_forall_mul_pow_le

L360 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.le_of_forall_mul_pow_le

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function

Lean source · statement

theorem le_of_forall_mul_pow_le {a b C D : ℕ} (hD : 0 < D) (h : ∀ k : ℕ, D * a ^ k ≤ C * b ^ k) :
    a ≤ b

abbrev

Pr

L407 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.Pr

Documentation

The ℓ-primary component of A.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Assembly
variable {A : Type*} [AddCommGroup A] (ℓ : ℕ) [hℓ : Fact ℓ.Prime]

Lean source · statement

abbrev Pr : AddSubgroup A

def

Hs

L410 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.Hs

Documentation

The image of the ℓ-primary component under multiplication by ℓ ^ n₀.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Assembly
variable {A : Type*} [AddCommGroup A] (ℓ : ℕ) [hℓ : Fact ℓ.Prime]

Lean source · statement

def Hs (n₀ : ℕ) : AddSubgroup A

theorem

mem_Pr

L412 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.mem_Pr

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Assembly
variable {A : Type*} [AddCommGroup A] (ℓ : ℕ) [hℓ : Fact ℓ.Prime]
omit hℓ in

Lean source · statement

theorem mem_Pr {x : A} : x ∈ Pr (A := A) ℓ ↔ ∃ m : ℕ, ℓ ^ m • x = 0

theorem

mem_Hs

L415 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.mem_Hs

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Assembly
variable {A : Type*} [AddCommGroup A] (ℓ : ℕ) [hℓ : Fact ℓ.Prime]
omit hℓ in

Lean source · statement

theorem mem_Hs {n₀ : ℕ} {x : A} :
    x ∈ Hs (A := A) ℓ n₀ ↔ ∃ y : A, y ∈ Pr (A := A) ℓ ∧ ℓ ^ n₀ • y = x

theorem

Hs_le_Pr

L420 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.Hs_le_Pr

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Assembly
variable {A : Type*} [AddCommGroup A] (ℓ : ℕ) [hℓ : Fact ℓ.Prime]
omit hℓ in

Lean source · statement

theorem Hs_le_Pr (n₀ : ℕ) : Hs (A := A) ℓ n₀ ≤ Pr ℓ

theorem

map_mem_Pr

L425 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.map_mem_Pr

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Assembly
variable {A : Type*} [AddCommGroup A] (ℓ : ℕ) [hℓ : Fact ℓ.Prime]
omit hℓ in

Lean source · statement

theorem map_mem_Pr (σ : A →+ A) {x : A} (hx : x ∈ Pr (A := A) ℓ) : σ x ∈ Pr (A := A) ℓ

theorem

map_mem_Hs

L429 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.map_mem_Hs

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Assembly
variable {A : Type*} [AddCommGroup A] (ℓ : ℕ) [hℓ : Fact ℓ.Prime]
omit hℓ in

Lean source · statement

theorem map_mem_Hs (σ : A →+ A) {n₀ : ℕ} {x : A} (hx : x ∈ Hs (A := A) ℓ n₀) :
    σ x ∈ Hs (A := A) ℓ n₀

def

res

L435 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.res

Documentation

Restrict an additive endomorphism to the image Hs ℓ n₀ of the primary component.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Assembly
variable {A : Type*} [AddCommGroup A] (ℓ : ℕ) [hℓ : Fact ℓ.Prime]

Lean source · statement

def res (n₀ : ℕ) (σ : AddMonoid.End A) : AddMonoid.End (Hs (A := A) ℓ n₀)

theorem

coe_res

L438 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.coe_res

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Assembly
variable {A : Type*} [AddCommGroup A] (ℓ : ℕ) [hℓ : Fact ℓ.Prime]
omit hℓ in

Lean source · statement

theorem coe_res (n₀ : ℕ) (σ : AddMonoid.End A) (x : Hs (A := A) ℓ n₀) :
    ((res ℓ n₀ σ x : Hs (A := A) ℓ n₀) : A) = σ x

theorem

res_one

L441 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.res_one

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Assembly
variable {A : Type*} [AddCommGroup A] (ℓ : ℕ) [hℓ : Fact ℓ.Prime]
omit hℓ in

Lean source · statement

theorem res_one (n₀ : ℕ) : res (A := A) ℓ n₀ 1 = 1

theorem

res_mul

L447 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.res_mul

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Assembly
variable {A : Type*} [AddCommGroup A] (ℓ : ℕ) [hℓ : Fact ℓ.Prime]
omit hℓ in

Lean source · statement

theorem res_mul (n₀ : ℕ) (σ σ' : AddMonoid.End A) :
    res (A := A) ℓ n₀ (σ * σ') = res ℓ n₀ σ * res ℓ n₀ σ'

theorem

res_pow

L454 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.res_pow

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Assembly
variable {A : Type*} [AddCommGroup A] (ℓ : ℕ) [hℓ : Fact ℓ.Prime]
omit hℓ in

Lean source · statement

theorem res_pow (n₀ : ℕ) (σ : AddMonoid.End A) (j : ℕ) :
    res (A := A) ℓ n₀ (σ ^ j) = res ℓ n₀ σ ^ j

theorem

coe_res_pow

L460 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.coe_res_pow

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Assembly
variable {A : Type*} [AddCommGroup A] (ℓ : ℕ) [hℓ : Fact ℓ.Prime]
omit hℓ in

Lean source · statement

theorem coe_res_pow (n₀ : ℕ) (σ : AddMonoid.End A) (j : ℕ) (x : Hs (A := A) ℓ n₀) :
    (((res ℓ n₀ σ ^ j) x : Hs (A := A) ℓ n₀) : A) = (σ ^ j) x

theorem

Hs_props

L468 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.Hs_props

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Assembly
variable {A : Type*} [AddCommGroup A] (ℓ : ℕ) [hℓ : Fact ℓ.Prime]
variable [Finite (tor A ℓ)]
omit [Finite ↥(tor A ℓ)] in
omit hℓ in

Lean source · statement

theorem Hs_props {n₀ : ℕ} (hn₀ : ∀ n, n₀ ≤ n → I (A := A) ℓ n = I ℓ n₀) :
    (∀ x ∈ Hs (A := A) ℓ n₀, ∃ y ∈ Hs (A := A) ℓ n₀, ℓ • y = x) ∧
    Hs (A := A) ℓ n₀ ⊓ tor A ℓ = I ℓ n₀

theorem

finite_quotient

L518 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.finite_quotient

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Assembly
variable {A : Type*} [AddCommGroup A] (ℓ : ℕ) [hℓ : Fact ℓ.Prime]
variable [Finite (tor A ℓ)]
omit hℓ in

Lean source · statement

theorem finite_quotient {n₀ : ℕ} (hn₀ : ∀ n, n₀ ≤ n → I (A := A) ℓ n = I ℓ n₀) :
    Finite (Pr (A := A) ℓ ⧸ (Hs (A := A) ℓ n₀).addSubgroupOf (Pr (A := A) ℓ))

theorem

main

L580 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent.P2mTorsionGrowth.main

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
namespace P2mTorsionGrowth
open AddSubgroup Function
section Main
variable {A : Type*} [AddCommGroup A] (ℓ : ℕ) [hℓ : Fact ℓ.Prime]

Lean source · statement

theorem main [Finite (tor A ℓ)] (r : ℕ) (τ : A →+ A)
    (hle : Nat.card (tor A ℓ) ≤ ℓ ^ r)
    (hτ : ∀ x : A, ℓ ^ 2 • x = 0 → τ x = x)
    (c k₀ : ℕ) (hfix : ∀ k : ℕ,
      Nat.card {x : A // x ∈ AddCommGroup.primaryComponent A ℓ ∧ (⇑τ)^[ℓ ^ (k₀ + k)] x = x} =
        ℓ ^ (r * k + c)) (n : ℕ) :
    Nat.card (T (A := A) ℓ n) = ℓ ^ (r * n)

theorem

natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent

L733 ↗

AddCommGroup.natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
open P2mTorsionGrowth in

Lean source · statement

theorem _root_.AddCommGroup.natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
    {A : Type*} [AddCommGroup A] (ℓ : ℕ) [Fact ℓ.Prime] (r : ℕ) (τ : A →+ A)
    (hfin : Finite (Submodule.torsionBy ℤ A (ℓ : ℤ)))
    (hle : Nat.card (Submodule.torsionBy ℤ A (ℓ : ℤ)) ≤ ℓ ^ r)
    (hτ : ∀ x : A, ℓ ^ 2 • x = 0 → τ x = x)
    (hfix : ∃ c k₀ : ℕ, ∀ k : ℕ,
      Nat.card {x : A // x ∈ AddCommGroup.primaryComponent A ℓ ∧ (⇑τ)^[ℓ ^ (k₀ + k)] x = x} =
        ℓ ^ (r * k + c))
    (n : ℕ) :
    Nat.card (Submodule.torsionBy ℤ A ((ℓ ^ n : ℕ) : ℤ)) = ℓ ^ (r * n)

Module documentation

Add Comm Group nat Card torsion By pow eq pow of nat Card fixed primary Component

Declarations