Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-04 20:50 9f78ea86

View on Github →

chore(algebra/ne_zero): move the dependencies out (#17177) This removes basically everything from algebra.ne_zero (since it doesn't require any imports for the definition), and inverts the dependencies on all the theorems in the file, putting them wherever they can fit earliest. Supercedes #17175 and (I think) #17176.

Estimated changes

Modified src/algebra/char_zero/defs.lean

Modified src/algebra/group_power/ring.lean

Modified src/algebra/group_with_zero/basic.lean

modified theorem one_ne_zero

Modified src/algebra/hom/group.lean

added theorem ne_zero.of_injective

added theorem ne_zero.of_map

Modified src/algebra/invertible.lean

Modified src/algebra/ne_zero.lean

deleted theorem ne_zero.nat_of_injective

deleted theorem ne_zero.nat_of_ne_zero

deleted theorem ne_zero.ne'

deleted theorem ne_zero.of_gt

deleted theorem ne_zero.of_injective

deleted theorem ne_zero.of_map

deleted theorem ne_zero.of_ne_zero_coe

modified theorem ne_zero.of_pos

deleted theorem ne_zero.pos

deleted theorem ne_zero.pos_of_ne_zero_coe

Modified src/algebra/order/monoid/canonical.lean

added theorem ne_zero.of_gt

added theorem ne_zero.pos

Modified src/algebra/order/ring.lean

Modified src/data/fin/basic.lean

Modified src/data/nat/cast.lean

added theorem ne_zero.nat_of_injective

added theorem ne_zero.nat_of_ne_zero

Modified src/data/nat/cast/defs.lean

added theorem ne_zero.ne'

added theorem ne_zero.of_ne_zero_coe

added theorem ne_zero.pos_of_ne_zero_coe

Modified src/data/pnat/basic.lean