Module

Submodule_finite_torsionBy_pow_of_finite_torsionBy.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Submodule_finite_torsionBy_pow_of_finite_torsionBy

1 declaration indexed from sourceView source ↗

Module documentation

Submodule finite torsion By pow of finite torsion By

Imports2

Mathlib.Algebra.Module.Torsion.Basic
Mathlib.Tactic.Abel

Imported by1

Nyll.AlgebraicCurves.Foundations.Algebra.All

theorem

finite_torsionBy_pow_of_finite_torsionBy

L25 ↗

Submodule.finite_torsionBy_pow_of_finite_torsionBy

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Submodule_finite_torsionBy_pow_of_finite_torsionBy

Lean source · statement

theorem _root_.Submodule.finite_torsionBy_pow_of_finite_torsionBy
    {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M] (a : R)
    (h : Finite (Submodule.torsionBy R M a)) (k : ℕ) :
    Finite (Submodule.torsionBy R M (a ^ k))

Module documentation

Submodule finite torsion By pow of finite torsion By

Declarations

finite_torsionBy_pow_of_finite_torsionBy