Commit 2024-05-30 06:23 cc6c82f9

View on Github →

feat: corollary of Chinese Remainder Theorem (#13306)

Estimated changes

Modified Mathlib/RingTheory/Ideal/QuotientOperations.lean

added theorem Ideal.exists_forall_sub_mem_ideal

added theorem Ideal.pi_quotient_surjective