Commit 2020-10-11 16:27 918e5d82

View on Github →

chore(data/finsupp): replace eq_zero_of_zero_eq_one with finsupp.unique_of_right (#4563) Also add a lemma semimodule.subsingleton: if R is a subsingleton semiring, then any semimodule over R is a subsingleton.

Estimated changes

Modified src/algebra/group/units.lean

added theorem is_unit_of_subsingleton

Modified src/algebra/group_with_zero.lean

added theorem subsingleton_iff_zero_eq_one

deleted theorem subsingleton_of_zero_eq_one

Modified src/algebra/module/basic.lean

added theorem semimodule.subsingleton

Modified src/data/finsupp/basic.lean

Modified src/linear_algebra/linear_independent.lean

added theorem linear_independent_of_subsingleton

deleted theorem linear_independent_of_zero_eq_one