Mathlib v3 is deprecated. Go to Mathlib v4

Theorem zero_ne_one_or_forall_eq_0

Modification history

2020-07-01 23:16
src/algebra/group_with_zero.lean
chore(algebra/*): deduplicate `*_with_zero`/`semiring`/`field` (#3259) …
Modified zero_ne_one_or_forall_eq_0View on Github →
2018-09-20 17:48
algebra/ring.lean
refactor(linear_algebra/basic): move some lemmas to the right place
Modified zero_ne_one_or_forall_eq_0View on Github →
2017-12-08 17:29
algebra/linear_algebra/basic.lean
refactor(algebra/linear_algebra): move zero_not_mem_of_linear_independent from vector_space to module (zero_ne_one should be a typeclass in Prop not in Type)
Added zero_ne_one_or_forall_eq_0View on Github →