Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-01 00:30 8e381f6e

View on Github →

feat(ring_theory/algebra_operations): multiplication of submodules of an algebra (#658)

Estimated changes

added theorem submodule.add_eq_sup
added theorem submodule.zero_eq_bot
added theorem algebra.bot_mul
added theorem algebra.fg_mul
added theorem algebra.mul_bot
added theorem algebra.mul_le
added theorem algebra.mul_le_mul
added theorem algebra.mul_mem_mul
added theorem algebra.mul_sup
added theorem algebra.span_mul_span
added theorem algebra.sup_mul
deleted theorem submodule.add_eq_sup
deleted theorem submodule.zero_eq_bot