Commit 2023-03-15 12:15 a85bc07a

View on Github →

feat: port RingTheory.Ideal.Prod (#2877)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Ideal/Prod.lean

added def Ideal.idealProdEquiv

added theorem Ideal.idealProdEquiv_symm_apply

added theorem Ideal.ideal_prod_eq

added theorem Ideal.ideal_prod_prime

added theorem Ideal.ideal_prod_prime_aux

added theorem Ideal.isPrime_ideal_prod_top'

added theorem Ideal.isPrime_ideal_prod_top

added theorem Ideal.isPrime_of_isPrime_prod_top'

added theorem Ideal.isPrime_of_isPrime_prod_top

added theorem Ideal.map_fst_prod

added theorem Ideal.map_prodComm_prod

added theorem Ideal.map_snd_prod

added theorem Ideal.mem_prod

added theorem Ideal.prod.ext_iff

added def Ideal.prod

added theorem Ideal.prod_top_top