Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-26 18:26 902b01d8

View on Github →

chore(algebra/group): rename is_unit_unit to units.is_unit (#6886)

Estimated changes

Modified src/algebra/group/units.lean

deleted theorem is_unit_unit

Modified src/algebra/group/units_hom.lean

Modified src/algebra/group_with_zero/basic.lean

modified theorem is_unit.mk0

Modified src/algebra/ring/basic.lean

Modified src/analysis/normed_space/units.lean

Modified src/data/equiv/mul_add.lean

Modified src/data/padics/padic_integers.lean

Modified src/dynamics/circle/rotation_number/translation_number.lean

Modified src/linear_algebra/nonsingular_inverse.lean

Modified src/ring_theory/discrete_valuation_ring.lean

Modified src/ring_theory/multiplicity.lean

Modified src/ring_theory/power_series/basic.lean