Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-22 20:06 45470769

View on Github →

chore(*): use zero_lt_two/two_ne_zero lemmas more (#13609)

Estimated changes

Modified src/algebra/group_with_zero/basic.lean

added theorem mul_self_ne_zero

added theorem zero_ne_mul_self

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

Modified src/data/nat/modeq.lean

Modified src/data/nat/sqrt.lean

Modified src/number_theory/fermat4.lean

Modified src/number_theory/lucas_lehmer.lean

Modified src/number_theory/pythagorean_triples.lean