Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-05 19:45 221ec606

View on Github →

feat(ring_theory/ideal): ideals in product rings (#4431)

Estimated changes

Modified src/algebra/group/prod.lean

added theorem mul_equiv.coe_prod_comm

added theorem mul_equiv.coe_prod_comm_symm

added def mul_equiv.prod_comm

Modified src/algebra/ring/prod.lean

added theorem ring_equiv.coe_coe_prod_comm

added theorem ring_equiv.coe_coe_prod_comm_symm

added theorem ring_equiv.coe_prod_comm

added theorem ring_equiv.coe_prod_comm_symm

added theorem ring_equiv.fst_comp_coe_prod_comm

added def ring_equiv.prod_comm

added theorem ring_equiv.snd_comp_coe_prod_comm

Modified src/algebraic_geometry/prime_spectrum.lean

added theorem prime_spectrum.prime_spectrum_prod_symm_inl_as_ideal

added theorem prime_spectrum.prime_spectrum_prod_symm_inr_as_ideal

Modified src/ring_theory/ideal/operations.lean

added theorem ideal.map_is_prime_of_equiv

added theorem ring_hom.ker_coe_equiv

Created src/ring_theory/ideal/prod.lean

added theorem ideal.ideal_prod_eq

added def ideal.ideal_prod_equiv

added theorem ideal.ideal_prod_equiv_symm_apply

added theorem ideal.ideal_prod_prime

added theorem ideal.ideal_prod_prime_aux

added theorem ideal.is_prime_ideal_prod_top'

added theorem ideal.is_prime_ideal_prod_top

added theorem ideal.is_prime_of_is_prime_prod_top'

added theorem ideal.is_prime_of_is_prime_prod_top

added theorem ideal.map_fst_prod

added theorem ideal.map_prod_comm_prod

added theorem ideal.map_snd_prod

added theorem ideal.mem_prod

added theorem ideal.prime_ideals_equiv_symm_inl

added theorem ideal.prime_ideals_equiv_symm_inr

added theorem ideal.prod.ext_iff

added def ideal.prod

added theorem ideal.prod_top_top