Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-20 17:48 bd26b065

View on Github →

refactor(linear_algebra/basic): move some lemmas to the right place

Estimated changes

Modified algebra/ring.lean

added theorem zero_ne_one_or_forall_eq_0

Modified data/seq/computation.lean

Modified data/set/basic.lean

added theorem set.diff_self

Modified linear_algebra/basic.lean

deleted theorem set.diff_self

deleted theorem zero_ne_one_or_forall_eq_0