Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-04-03 05:37 2c735dc9

View on Github →

feat(ring_theory/algebra_operations): submodules form a semiring (#856)

Estimated changes

Modified src/algebra/pointwise.lean

added theorem set.pointwise_mul_finite

Modified src/ring_theory/algebra_operations.lean

deleted theorem algebra.bot_mul

deleted theorem algebra.fg_mul

deleted theorem algebra.mul_bot

deleted theorem algebra.mul_le

deleted theorem algebra.mul_le_mul

deleted theorem algebra.mul_le_mul_left

deleted theorem algebra.mul_le_mul_right

deleted theorem algebra.mul_mem_mul

deleted theorem algebra.mul_mem_mul_rev

deleted theorem algebra.mul_sup

deleted theorem algebra.span_mul_span

deleted theorem algebra.sup_mul

added theorem submodule.bot_mul

added theorem submodule.mul_bot

added theorem submodule.mul_le

added theorem submodule.mul_le_mul

added theorem submodule.mul_le_mul_left

added theorem submodule.mul_le_mul_right

added theorem submodule.mul_mem_mul

added theorem submodule.mul_mem_mul_rev

added theorem submodule.mul_sup

added theorem submodule.one_eq_map_top

added theorem submodule.one_eq_span

added theorem submodule.one_le

added theorem submodule.span_mul_span

added theorem submodule.sup_mul

Modified src/ring_theory/ideal_operations.lean

modified theorem ideal.one_eq_top

modified theorem submodule.bot_smul

modified theorem submodule.smul_bot

modified theorem submodule.top_smul

Modified src/ring_theory/noetherian.lean

added theorem submodule.fg_mul