Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-19 09:29 5228d557

View on Github →

feat(linear_algebra/basic): add span_zero (#3306) simp now proves span_zero for both submodules and ideals

Estimated changes

Modified src/linear_algebra/basic.lean

modified theorem submodule.span_singleton_eq_bot

added theorem submodule.span_zero

Modified src/linear_algebra/basis.lean

Modified src/ring_theory/fractional_ideal.lean

Modified src/ring_theory/ideals.lean

modified theorem ideal.span_singleton_eq_bot

added theorem ideal.span_zero