Commit 2024-01-06 09:51 82354164

View on Github →

feat: Provide glue between AddCommGroup and Module ℤ (#9345)

Estimated changes

Modified Mathlib/Algebra/DirectSum/LinearMap.lean

Modified Mathlib/Algebra/Lie/Killing.lean

Modified Mathlib/Algebra/Lie/Weights/Linear.lean

Modified Mathlib/Algebra/Module/Submodule/Lattice.lean

added theorem Submodule.bot_toAddSubgroup

added theorem Submodule.top_toAddSubgroup

Modified Mathlib/Algebra/Module/Torsion.lean

added theorem Submodule.AddMonoid.IsTorsionFree_iff_noZeroSMulDivisors

added theorem Submodule.torsion_int

Modified Mathlib/Algebra/Module/Zlattice.lean

Modified Mathlib/GroupTheory/OrderOfElement.lean

added theorem isOfFinOrder_iff_zpow_eq_one

Modified Mathlib/GroupTheory/Torsion.lean

added theorem Monoid.isTorsionFree_iff_torsion_eq_bot

Modified Mathlib/LinearAlgebra/FreeModule/PID.lean

added theorem Module.free_iff_noZeroSMulDivisors

deleted theorem Module.free_of_finite_type_torsion_free'

Modified Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean