Commit 2021-11-10 14:52 e1fea3a1

View on Github →

feat(ring_theory/ideal): the product and infimum of principal ideals (#9852) Three useful lemmas for applying the Chinese remainder theorem when an ideal is generated by one, non-prime, element.

Estimated changes

Modified src/algebra/algebra/operations.lean

added theorem submodule.prod_span

added theorem submodule.prod_span_singleton

Modified src/algebra/module/submodule_lattice.lean

added theorem submodule.finset_inf_coe

added theorem submodule.mem_finset_inf

Modified src/algebra/pointwise.lean

added theorem set.finset_prod_singleton

Modified src/ring_theory/ideal/operations.lean

added theorem ideal.finset_inf_span_singleton

added theorem ideal.infi_span_singleton

added theorem ideal.prod_span

added theorem ideal.prod_span_singleton

Modified src/ring_theory/multiplicity.lean