Module

card_torsion_mul_of_divisible.lean

Nyll.AlgebraicCurves.Foundations.Algebra.card_torsion_mul_of_divisible

1 declaration indexed from sourceView source ↗

Module documentation

card torsion mul of divisible

Imports3

Mathlib.Algebra.Module.NatInt
Mathlib.GroupTheory.Coset.Card
Mathlib.GroupTheory.QuotientGroup.Basic

Imported by1

Nyll.AlgebraicCurves.Foundations.Algebra.All

theorem

card_torsion_mul_of_divisible

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.card_torsion_mul_of_divisible
open Function

Lean source · statement

theorem _root_.card_torsion_mul_of_divisible
    {A : Type*} [AddCommGroup A]
    (hdiv : ∀ m : ℕ, m ≠ 0 → ∀ x : A, ∃ y : A, m • y = x)
    (a b : ℕ) (ha : a ≠ 0)
    (hfa : Finite {x : A // a • x = 0}) (hfb : Finite {x : A // b • x = 0}) :
    Finite {x : A // (a * b) • x = 0} ∧
      Nat.card {x : A // (a * b) • x = 0} =
        Nat.card {x : A // a • x = 0} * Nat.card {x : A // b • x = 0}