Commit 2022-03-03 17:48 16d48d7e

View on Github →

feat(algebra/star/basic + analysis/normed_space/star/basic): add two eq_zero/ne_zero lemmas (#12412) Added two lemmas about elements being zero or non-zero. Golf a proof.

Estimated changes

Modified src/algebra/star/basic.lean

modified theorem star_div

added theorem star_eq_zero

added theorem star_ne_zero

Modified src/analysis/normed_space/star/basic.lean