Theorem Ideal.index_pow_le

Modification history

2025-02-03 13:40
Mathlib/RingTheory/Ideal/Quotient/Index.lean
feat(RingTheory): index of power of ideal (#20290)
Added Ideal.index_pow_leView on Github →