Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-02-03 13:40
a6276f4c
View on Github →
feat(RingTheory): index of power of ideal (
#20290
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/RingTheory/Ideal/Quotient/Index.lean
added
theorem
Ideal.finite_quotient_pow
added
theorem
Ideal.index_pow_le
added
theorem
Submodule.finite_quotient_smul
added
theorem
Submodule.index_smul_le