Theorem Ideal.iInf_span_singleton_natCast

Modification history

2023-10-10 17:21
Mathlib/RingTheory/Ideal/Operations.lean
feat: Chinese remainder for ZMod. (#7599)
Added Ideal.iInf_span_singleton_natCastView on Github →